let a be Element of C; :: thesis: for X being set st ( for x being set holds
( x in X iff ( x in H₁(a) & S₁[a,x] ) ) ) holds
S₂[a,a, id X]
let X be set ; :: thesis: ( ( for x being set holds
( x in X iff ( x in H₁(a) & S₁[a,x] ) ) ) implies S₂[a,a, id X] )
assume A10: for x being set holds
( x in X iff ( x in Union (disjoin the Arrows of C) & S₁[a,x] ) ) ; :: thesis: S₂[a,a, id X]
reconsider fa = a as object of C ;
take fa ; :: thesis: ex fb being object of C ex g being Morphism of fa,fb st
( fa = a & fb = a & <^fa,fb^> <> {} & ( for o being object of C st <^o,fa^> <> {} holds
for h being Morphism of o,fa holds (id X) . [h,[o,fa]] = [(g * h),[o,fb]] ) )
take fa ; :: thesis: ex g being Morphism of fa,fa st
( fa = a & fa = a & <^fa,fa^> <> {} & ( for o being object of C st <^o,fa^> <> {} holds
for h being Morphism of o,fa holds (id X) . [h,[o,fa]] = [(g * h),[o,fa]] ) )
take g = idm fa; :: thesis: ( fa = a & fa = a & <^fa,fa^> <> {} & ( for o being object of C st <^o,fa^> <> {} holds
for h being Morphism of o,fa holds (id X) . [h,[o,fa]] = [(g * h),[o,fa]] ) )
thus ( fa = a & fa = a & <^fa,fa^> <> {} ) ; :: thesis: for o being object of C st <^o,fa^> <> {} holds
for h being Morphism of o,fa holds (id X) . [h,[o,fa]] = [(g * h),[o,fa]]
let o be object of C; :: thesis: ( <^o,fa^> <> {} implies for h being Morphism of o,fa holds (id X) . [h,[o,fa]] = [(g * h),[o,fa]] )
assume A11: <^o,fa^> <> {} ; :: thesis: for h being Morphism of o,fa holds (id X) . [h,[o,fa]] = [(g * h),[o,fa]]
let h be Morphism of o,fa; :: thesis: (id X) . [h,[o,fa]] = [(g * h),[o,fa]]
A12: ( [h,[o,fa]] `1 = h & [h,[o,fa]] `2 = [o,fa] ) by MCART_1:7;
A13: [h,[o,fa]] `22 = fa by MCART_1:89;
dom the Arrows of C = [:the carrier of C,the carrier of C:] by PARTFUN1:def 4;
then ( [o,fa] in dom the Arrows of C & h in the Arrows of C . [o,fa] ) by A11, ZFMISC_1:def 2;
then [h,[o,fa]] in Union (disjoin the Arrows of C) by A12, CARD_3:33;
then [h,[o,fa]] in X by A10, A13;
hence (id X) . [h,[o,fa]] = [h,[o,fa]] by FUNCT_1:35
.= [(g * h),[o,fa]] by A11, ALTCAT_1:24 ;
:: thesis: verum