let a, b, c be Element of C; :: thesis: for f, g being Function st S₂[a,b,f] & S₂[b,c,g] holds
S₂[a,c,g * f]
let f, g be Function; :: thesis: ( S₂[a,b,f] & S₂[b,c,g] implies S₂[a,c,g * f] )
given fa, fb being Object of C, ff being Morphism of fa,fb such that A2: fa = a and
A3: fb = b and
A4: <^fa,fb^> <> {} and
A5: for o being Object of C st <^o,fa^> <> {} holds
for h being Morphism of o,fa holds f . [h,[o,fa]] = [(ff * h),[o,fb]] ; :: thesis: ( not S₂[b,c,g] or S₂[a,c,g * f] )
given ga, gb being Object of C, gf being Morphism of ga,gb such that A6: ga = b and
A7: gb = c and
A8: <^ga,gb^> <> {} and
A9: for o being Object of C st <^o,ga^> <> {} holds
for h being Morphism of o,ga holds g . [h,[o,ga]] = [(gf * h),[o,gb]] ; :: thesis: S₂[a,c,g * f]
reconsider gf = gf as Morphism of fb,gb by A3, A6;
take fa ; :: thesis: ex fb being Object of C ex g being Morphism of fa,fb st
( fa = a & fb = c & <^fa,fb^> <> {} & ( for o being Object of C st <^o,fa^> <> {} holds
for h being Morphism of o,fa holds (g * f) . [h,[o,fa]] = [(g * h),[o,fb]] ) )
take gb ; :: thesis: ex g being Morphism of fa,gb st
( fa = a & gb = c & <^fa,gb^> <> {} & ( for o being Object of C st <^o,fa^> <> {} holds
for h being Morphism of o,fa holds (g * f) . [h,[o,fa]] = [(g * h),[o,gb]] ) )
take k = gf * ff; :: thesis: ( fa = a & gb = c & <^fa,gb^> <> {} & ( for o being Object of C st <^o,fa^> <> {} holds
for h being Morphism of o,fa holds (g * f) . [h,[o,fa]] = [(k * h),[o,gb]] ) )
thus ( fa = a & gb = c & <^fa,gb^> <> {} ) by A2, A3, A4, A6, A7, A8, ALTCAT_1:def 2; :: thesis: for o being Object of C st <^o,fa^> <> {} holds
for h being Morphism of o,fa holds (g * f) . [h,[o,fa]] = [(k * h),[o,gb]]
let o be Object of C; :: thesis: ( <^o,fa^> <> {} implies for h being Morphism of o,fa holds (g * f) . [h,[o,fa]] = [(k * h),[o,gb]] )
assume A10: <^o,fa^> <> {} ; :: thesis: for h being Morphism of o,fa holds (g * f) . [h,[o,fa]] = [(k * h),[o,gb]]
A11: <^o,fb^> <> {} by A4, A10, ALTCAT_1:def 2;
let h be Morphism of o,fa; :: thesis: (g * f) . [h,[o,fa]] = [(k * h),[o,gb]]
A12: f . [h,[o,fa]] = [(ff * h),[o,fb]] by A5, A10;
then [h,[o,fa]] in dom f by FUNCT_1:def 2;
hence (g * f) . [h,[o,fa]] = g . [(ff * h),[o,fb]] by A12, FUNCT_1:13
.= [(gf * (ff * h)),[o,gb]] by A3, A6, A9, A11
.= [(k * h),[o,gb]] by A3, A4, A6, A8, A10, ALTCAT_1:21 ;
:: thesis: verum