let R be Ring; :: thesis: for a being Data-Location of R holds Values a = the carrier of R
let a be Data-Location of R; :: thesis: Values a = the carrier of R
( a in Data-Locations & the_Values_of (SCM R) = () * SCM-OK ) by ;
hence Values a = the carrier of R by ; :: thesis: verum
{"ft_lang_label":"__label__en","ft_lang_prob":0.7330723,"math_prob":0.9884997,"size":300,"snap":"2022-40-2023-06","text_gpt3_token_len":111,"char_repetition_ratio":0.1554054,"word_repetition_ratio":0.16071428,"special_character_ratio":0.33,"punctuation_ratio":0.14084508,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.99711436,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2022-09-30T15:22:45Z\",\"WARC-Record-ID\":\"<urn:uuid:f3516e8e-f1c6-40ef-b932-4f8ef7962390>\",\"Content-Length\":\"3618\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:541a76a7-2039-454c-9644-4fc27b8f60c1>\",\"WARC-Concurrent-To\":\"<urn:uuid:363c5415-7570-456b-9c4c-14aeff57cec1>\",\"WARC-IP-Address\":\"193.219.28.149\",\"WARC-Target-URI\":\"http://mizar.org/version/current/html/proofs/scmring3/1\",\"WARC-Payload-Digest\":\"sha1:UZF4FG5PJOQR45YAMI6SKJMA65WYPPZM\",\"WARC-Block-Digest\":\"sha1:NTNTM637WO4X2I3G4IEU3AEOWCMRRSWR\",\"WARC-Identified-Payload-Type\":\"application/xml\",\"warc_filename\":\"/cc_download/warc_2022/CC-MAIN-2022-40/CC-MAIN-2022-40_segments_1664030335491.4_warc_CC-MAIN-20220930145518-20220930175518-00620.warc.gz\"}"}