let A be category; for a being object of
for x being set holds
( x in (Concretized A) -carrier_of a iff ex b being object of ex f being Morphism of , st
( <^b,a^> <> {} & x = [f,[b,a]] ) )
let a be object of ; for x being set holds
( x in (Concretized A) -carrier_of a iff ex b being object of ex f being Morphism of , st
( <^b,a^> <> {} & x = [f,[b,a]] ) )
let x be set ; ( x in (Concretized A) -carrier_of a iff ex b being object of ex f being Morphism of , st
( <^b,a^> <> {} & x = [f,[b,a]] ) )
set B = Concretized A;
reconsider ac = a as object of 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 ( ex b being object of ex f being Morphism of , st
( <^b,a^> <> {} & x = [f,[b,a]] ) implies x in (Concretized A) -carrier_of a )
assume A3:
x in (Concretized A) -carrier_of a
;
ex b being object of ex f being Morphism of , st
( <^b,a^> <> {} & x = [f,[b,a]] )then A4:
x `2 in dom the
Arrows of
A
by A1, CARD_3:33;
A5:
x `1 in the
Arrows of
A . (x `2 )
by A1, A3, CARD_3:33;
A6:
x = [(x `1 ),(x `2 )]
by A1, A3, CARD_3:33;
consider b,
c being
set such that A7:
b in the
carrier of
A
and
c in the
carrier of
A
and A8:
x `2 = [b,c]
by A2, A4, ZFMISC_1:def 2;
reconsider b =
b as
object of
by A7;
take b =
b;
ex f being Morphism of , st
( <^b,a^> <> {} & x = [f,[b,a]] )reconsider f =
x `1 as
Morphism of ,
by A1, A3, A5, A6, A8, MCART_1:89;
take f =
f;
( <^b,a^> <> {} & x = [f,[b,a]] )thus
(
<^b,a^> <> {} &
x = [f,[b,a]] )
by A1, A3, A5, A6, A8, MCART_1:89;
verum
end;
given b being object of , f being Morphism of , such that A9:
<^b,a^> <> {}
and
A10:
x = [f,[b,a]]
; x in (Concretized A) -carrier_of a
A11:
x `1 = f
by A10, MCART_1:7;
A12:
x `2 = [b,a]
by A10, MCART_1:7;
[b,a] in dom the Arrows of A
by A2, ZFMISC_1:def 2;
hence
x in (Concretized A) -carrier_of a
by A1, A9, A10, A11, A12, CARD_3:33, MCART_1:89; verum