let C be non empty pseudo-functional AltCatStr ; 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; ( <^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^> <> {}
; 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; 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; for f9, g9 being Function st f = f9 & g = g9 holds
g * f = g9 * f9
let f9, g9 be Function; ( f = f9 & g = g9 implies g * f = g9 * f9 )
assume A3:
( f = f9 & g = g9 )
; 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
; verum