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

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