set B = Concretized A;
set FF = Concretization A;
deffunc H1( set ) -> set = A;
A1:
for a being object of A holds (Concretization A) . a = H1(a)
by Def13;
deffunc H2( object of A, object of A, Morphism of A,c2) -> Element of <^((Concretization A) . A),((Concretization A) . c2)^> = (Concretization A) . c3;
A2:
for a, b being object of A st <^a,b^> <> {} holds
for f being Morphism of a,b holds (Concretization A) . f = H2(a,b,f)
;
A3:
for a, b being object of A st H1(a) = H1(b) holds
a = b
;
A4:
for a, b being object of A st <^a,b^> <> {} holds
for f, g being Morphism of a,b st H2(a,b,f) = H2(a,b,g) holds
f = g
proof
let a,
b be
object of
A;
:: thesis: ( <^a,b^> <> {} implies for f, g being Morphism of a,b st H2(a,b,f) = H2(a,b,g) holds
f = g )
assume A5:
<^a,b^> <> {}
;
:: thesis: for f, g being Morphism of a,b st H2(a,b,f) = H2(a,b,g) holds
f = g
let f,
g be
Morphism of
a,
b;
:: thesis: ( H2(a,b,f) = H2(a,b,g) implies f = g )
(
((Concretization A) . f) . [(idm a),[a,a]] = [f,[a,b]] &
((Concretization A) . g) . [(idm a),[a,a]] = [g,[a,b]] )
by A5, Def13;
hence
(
H2(
a,
b,
f)
= H2(
a,
b,
g) implies
f = g )
by ZFMISC_1:33;
:: thesis: verum
end;
A6:
for a, b being object of (Concretized A) st <^a,b^> <> {} holds
for f being Morphism of a,b ex c, d being object of A ex g being Morphism of c,d st
( a = H1(c) & b = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) )
proof
let a,
b be
object of
(Concretized A);
:: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b ex c, d being object of A ex g being Morphism of c,d st
( a = H1(c) & b = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) ) )
assume A7:
<^a,b^> <> {}
;
:: thesis: for f being Morphism of a,b ex c, d being object of A ex g being Morphism of c,d st
( a = H1(c) & b = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) )
reconsider c =
a,
d =
b as
object of
A by Def12;
let f be
Morphism of
a,
b;
:: thesis: ex c, d being object of A ex g being Morphism of c,d st
( a = H1(c) & b = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) )
take
c
;
:: thesis: ex d being object of A ex g being Morphism of c,d st
( a = H1(c) & b = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) )
take
d
;
:: thesis: ex g being Morphism of c,d st
( a = H1(c) & b = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) )
consider fa,
fb being
object of
A,
g being
Morphism of
fa,
fb such that A8:
(
fa = c &
fb = d &
<^fa,fb^> <> {} )
and A9:
for
o being
object of
A st
<^o,fa^> <> {} holds
for
h being
Morphism of
o,
fa holds
f . [h,[o,fa]] = [(g * h),[o,fb]]
by A7, Def12;
reconsider g =
g as
Morphism of
c,
d by A8;
take
g
;
:: thesis: ( a = H1(c) & b = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) )
(
<^c,c^> <> {} &
((Concretization A) . g) . [(idm c),[c,c]] = [g,[c,d]] &
g * (idm c) = g )
by A8, Def13, ALTCAT_1:def 19;
then A10:
((Concretization A) . g) . [(idm c),[c,c]] = f . [(idm c),[c,c]]
by A8, A9;
(
(Concretization A) . c = a &
(Concretization A) . d = b )
by Def13;
hence
(
a = H1(
c) &
b = H1(
d) &
<^c,d^> <> {} &
f = H2(
c,
d,
g) )
by A7, A8, A10, Th47;
:: thesis: verum
end;
thus
Concretization A is bijective
from YELLOW18:sch 10(A1, A2, A3, A4, A6); :: thesis: verum