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 & fb = b & <^fa,fb^> <> {} ) and
A3: 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 A4: ( ga = b & gb = c & <^ga,gb^> <> {} ) and
A5: 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 A2, A4;
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, A4, ALTCAT_1:def 4; :: 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 A6: <^o,fa^> <> {} ; :: thesis: for h being Morphism of o,fa holds (g * f) . [h,[o,fa]] = [(k * h),[o,gb]]
A7: <^o,fb^> <> {} by A2, A6, ALTCAT_1:def 4;
let h be Morphism of o,fa; :: thesis: (g * f) . [h,[o,fa]] = [(k * h),[o,gb]]
A8: f . [h,[o,fa]] = [(ff * h),[o,fb]] by A3, A6;
then [h,[o,fa]] in dom f by FUNCT_1:def 4;
hence (g * f) . [h,[o,fa]] = g . [(ff * h),[o,fb]] by A8, FUNCT_1:23
.= [(gf * (ff * h)),[o,gb]] by A2, A4, A5, A7
.= [(k * h),[o,gb]] by A2, A4, A6, ALTCAT_1:25 ;
:: thesis: verum