let B be non empty transitive SubCatStr of A; :: thesis:
let b1, b2, b3 be Object of B; :: according to ALTCAT_1:def 12 :: thesis: ( <^b1,b2^> = {} or <^b2,b3^> = {} or <^b1,b3^> = {} or for b1 being Element of <^b1,b2^>
for b2 being Element of <^b2,b3^>
for b3, b4 being set holds
( not b1 = b3 or not b2 = b4 or b2 * b1 = b3 * b4 ) )

assume that
A1: <^b1,b2^> <> {} and
A2: <^b2,b3^> <> {} and
A3: <^b1,b3^> <> {} ; :: thesis: for b1 being Element of <^b1,b2^>
for b2 being Element of <^b2,b3^>
for b3, b4 being set holds
( not b1 = b3 or not b2 = b4 or b2 * b1 = b3 * b4 )

reconsider a1 = b1, a2 = b2, a3 = b3 as Object of A by ALTCAT_2:29;
A4: ( <^a1,a2^> <> {} & <^a2,a3^> <> {} ) by ;
let f1 be Morphism of b1,b2; :: thesis: for b1 being Element of <^b2,b3^>
for b2, b3 being set holds
( not f1 = b2 or not b1 = b3 or b1 * f1 = b2 * b3 )

let f2 be Morphism of b2,b3; :: thesis: for b1, b2 being set holds
( not f1 = b1 or not f2 = b2 or f2 * f1 = b1 * b2 )

reconsider g2 = f2 as Morphism of a2,a3 by ;
reconsider g1 = f1 as Morphism of a1,a2 by ;
A5: <^a1,a3^> <> {} by ;
let f9, g9 be Function; :: thesis: ( not f1 = f9 or not f2 = g9 or f2 * f1 = f9 * g9 )
assume ( f1 = f9 & f2 = g9 ) ; :: thesis: f2 * f1 = f9 * g9
then g2 * g1 = g9 * f9 by ;
hence f2 * f1 = f9 * g9 by ; :: thesis: verum
{"ft_lang_label":"__label__en","ft_lang_prob":0.5635488,"math_prob":0.9994711,"size":1345,"snap":"2022-40-2023-06","text_gpt3_token_len":654,"char_repetition_ratio":0.13870247,"word_repetition_ratio":0.26875,"special_character_ratio":0.53011155,"punctuation_ratio":0.19648094,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.99885243,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2022-10-01T08:21:18Z\",\"WARC-Record-ID\":\"<urn:uuid:df8e198c-5681-44c6-8824-f26513bc3051>\",\"Content-Length\":\"18076\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:40191e5e-a1a5-4709-a748-0de810ee20ca>\",\"WARC-Concurrent-To\":\"<urn:uuid:acdee06f-7ac6-4f60-9e8c-dec80375c3e4>\",\"WARC-IP-Address\":\"193.219.28.149\",\"WARC-Target-URI\":\"http://mizar.org/version/current/html/proofs/yellow21/55_1_1\",\"WARC-Payload-Digest\":\"sha1:UCQPOAA3GFISEYJLZD54UMINXVYL4FTD\",\"WARC-Block-Digest\":\"sha1:6X6UW2FJNOW4TATTE6PCVXTK3XCZMU4W\",\"WARC-Identified-Payload-Type\":\"application/xml\",\"warc_filename\":\"/cc_download/warc_2022/CC-MAIN-2022-40/CC-MAIN-2022-40_segments_1664030335573.50_warc_CC-MAIN-20221001070422-20221001100422-00764.warc.gz\"}"}