let A be category; :: thesis:
let a be object of A; :: thesis:
let x be set ; :: thesis:
set B = Concretized A;
reconsider ac = a as object of (Concretized A) by Def12;
A1: ( x in the_carrier_of ac iff ( x in Union (disjoin the Arrows of A) & ac = x `22 ) ) by Def12;
A2: dom the Arrows of A = [:the carrier of A,the carrier of A:] by PARTFUN1:def 4;

hereby :: thesis:

assume A3: x in (Concretized A) -carrier_of a ; :: thesis:
then A4: ( x `2 in dom the Arrows of A & x `1 in the Arrows of A . (x `2 ) & x = [(x `1 ),(x `2 )] ) by A1, CARD_3:33;
then consider b, c being set such that
A5: ( b in the carrier of A & c in the carrier of A & x `2 = [b,c] ) by A2, ZFMISC_1:def 2;
reconsider b = b as object of A by A5;
take b = b; :: thesis:
reconsider f = x `1 as Morphism of b,a by A1, A3, A4, A5, MCART_1:89;
take f = f; :: thesis:
thus ( <^b,a^> <> {} & x = [f,[b,a]] ) by A1, A3, A4, A5, MCART_1:89; :: thesis:

end;

given b being object of A, f being Morphism of b,a such that A6: ( <^b,a^> <> {} & x = [f,[b,a]] ) ; :: thesis:
A7: ( x `1 = f & x `2 = [b,a] ) by A6, MCART_1:7;
then ( f in the Arrows of A . (x `2 ) & [b,a] in dom the Arrows of A ) by A2, A6, ZFMISC_1:def 2;
hence x in (Concretized A) -carrier_of a by A1, A6, A7, CARD_3:33, MCART_1:89; :: thesis: