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 A14: 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 A15: <^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]]
A16: [h,[o,fa]] `1 = h ;
A17: [h,[o,fa]] `2 = [o,fa] ;
A18: [h,[o,fa]] `22 = fa by MCART_1:85;
dom the Arrows of C = [: the carrier of C, the carrier of C:] by PARTFUN1:def 2;
then [o,fa] in dom the Arrows of C by ZFMISC_1:def 2;
then [h,[o,fa]] in Union (disjoin the Arrows of C) by A15, A16, A17, CARD_3:22;
then [h,[o,fa]] in X by A14, A18;
hence (id X) . [h,[o,fa]] = [h,[o,fa]] by FUNCT_1:18
.= [(g * h),[o,fa]] by A15, ALTCAT_1:20 ;
:: thesis: verum