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 f9, g9 being Function st f = f9 & g = g9 holds
g * f = g9 * f9
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 f9, g9 being Function st f = f9 & g = g9 holds
g * f = g9 * f9 )
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 f9, g9 being Function st f = f9 & g = g9 holds
g * f = g9 * f9
let f be Morphism of a1,a2; :: thesis: for g being Morphism of a2,a3
for f9, g9 being Function st f = f9 & g = g9 holds
g * f = g9 * f9
let g be Morphism of a2,a3; :: thesis: for f9, g9 being Function st f = f9 & g = g9 holds
g * f = g9 * f9
let f9, g9 be Function; :: thesis: ( f = f9 & g = g9 implies g * f = g9 * f9 )
assume A3: ( f = f9 & g = g9 ) ; :: thesis: g * f = g9 * f9
A4: [g,f] in [:<^a2,a3^>,<^a1,a2^>:] by A1, ZFMISC_1:87;
A5: the Comp of C . (a1,a2,a3) = (FuncComp ((Funcs (a1,a2)),(Funcs (a2,a3)))) | [:<^a2,a3^>,<^a1,a2^>:] by Def13;
( 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:60;
then consider f99, g99 being Function such that
A6: [g,f] = [g99,f99] and
A7: (FuncComp ((Funcs (a1,a2)),(Funcs (a2,a3)))) . [g,f] = g99 * f99 by A5, A4, Def9;
A8: ( g = g99 & f = f99 ) by A6, XTUPLE_0:1;
thus g * f = ( the Comp of C . (a1,a2,a3)) . (g,f) by A1, Def8
.= g9 * f9 by A5, A3, A4, A7, A8, FUNCT_1:49 ; :: thesis: verum