let a, b, c be Element of ; :: 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 , ff being Morphism of , such that A2: fa = a and
A3: fb = b and
A4: <^fa,fb^> <> {} and
A5: for o being object of st <^o,fa^> <> {} holds
for h being Morphism of , 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 , gf being Morphism of , such that A6: ga = b and
A7: gb = c and
A8: <^ga,gb^> <> {} and
A9: for o being object of st <^o,ga^> <> {} holds
for h being Morphism of , holds g . [h,[o,ga]] = [(gf * h),[o,gb]] ; :: thesis: S₂[a,c,g * f]
reconsider gf = gf as Morphism of , by A3, A6;
take fa ; :: thesis: ex fb being object of ex g being Morphism of , st
( fa = a & fb = c & <^fa,fb^> <> {} & ( for o being object of st <^o,fa^> <> {} holds
for h being Morphism of , holds (g * f) . [h,[o,fa]] = [(g * h),[o,fb]] ) )
take gb ; :: thesis: ex g being Morphism of , st
( fa = a & gb = c & <^fa,gb^> <> {} & ( for o being object of st <^o,fa^> <> {} holds
for h being Morphism of , 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 st <^o,fa^> <> {} holds
for h being Morphism of , 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 4; :: thesis: for o being object of st <^o,fa^> <> {} holds
for h being Morphism of , holds (g * f) . [h,[o,fa]] = [(k * h),[o,gb]]
let o be object of ; :: thesis: ( <^o,fa^> <> {} implies for h being Morphism of , holds (g * f) . [h,[o,fa]] = [(k * h),[o,gb]] )
assume A10: <^o,fa^> <> {} ; :: thesis: for h being Morphism of , holds (g * f) . [h,[o,fa]] = [(k * h),[o,gb]]
A11: <^o,fb^> <> {} by A4, A10, ALTCAT_1:def 4;
let h be Morphism of ,; :: 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 4;
hence (g * f) . [h,[o,fa]] = g . [(ff * h),[o,fb]] by A12, FUNCT_1:23
.= [(gf * (ff * h)),[o,gb]] by A3, A6, A9, A11
.= [(k * h),[o,gb]] by A3, A4, A6, A8, A10, ALTCAT_1:25 ;
:: thesis: verum