let C be non empty pseudo-functional AltCatStr ; :: thesis: for a1, a2, a3 being object of C st <^a1,a2^> <> {} & <^a2,a3^> <> {} & <^a1,a3^> <> {} holds
for f being Morphism of a1,a2
for g being Morphism of a2,a3
for f', g' being Function st f = f' & g = g' holds
g * f = g' * f'
let a1, a2, a3 be object of C; :: thesis: ( <^a1,a2^> <> {} & <^a2,a3^> <> {} & <^a1,a3^> <> {} implies for f being Morphism of a1,a2
for g being Morphism of a2,a3
for f', g' being Function st f = f' & g = g' holds
g * f = g' * f' )
assume that
A1: ( <^a1,a2^> <> {} & <^a2,a3^> <> {} ) and
A2: <^a1,a3^> <> {} ; :: thesis: for f being Morphism of a1,a2
for g being Morphism of a2,a3
for f', g' being Function st f = f' & g = g' holds
g * f = g' * f'
let f be Morphism of a1,a2; :: thesis: for g being Morphism of a2,a3
for f', g' being Function st f = f' & g = g' holds
g * f = g' * f'
let g be Morphism of a2,a3; :: thesis: for f', g' being Function st f = f' & g = g' holds
g * f = g' * f'
let f', g' be Function; :: thesis: ( f = f' & g = g' implies g * f = g' * f' )
assume A3: ( f = f' & g = g' ) ; :: thesis: g * f = g' * f'
A4: [g,f] in [:<^a2,a3^>,<^a1,a2^>:] by A1, ZFMISC_1:106;
A5: the Comp of C . a1,a2,a3 = (FuncComp (Funcs a1,a2),(Funcs a2,a3)) | [:<^a2,a3^>,<^a1,a2^>:] by Def15;
( dom ((FuncComp (Funcs a1,a2),(Funcs a2,a3)) | [:<^a2,a3^>,<^a1,a2^>:]) c= dom (FuncComp (Funcs a1,a2),(Funcs a2,a3)) & dom (the Comp of C . a1,a2,a3) = [:<^a2,a3^>,<^a1,a2^>:] ) by A2, FUNCT_2:def 1, RELAT_1:89;
then consider f'', g'' being Function such that
A6: [g,f] = [g'',f''] and
A7: (FuncComp (Funcs a1,a2),(Funcs a2,a3)) . [g,f] = g'' * f'' by A5, A4, Def11;
A8: ( g = g'' & f = f'' ) by A6, ZFMISC_1:33;
thus g * f = (the Comp of C . a1,a2,a3) . g,f by A1, Def10
.= g' * f' by A5, A3, A4, A7, A8, FUNCT_1:72 ; :: thesis: verum