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;
( <^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^> <> {}
;
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;
( H2(a,b,f) = H2(a,b,g) implies f = g )
A6:
((Concretization A) . f) . [(idm a),[a,a]] = [f,[a,b]]
by A5, Def13;
((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 A6, XTUPLE_0:1;
verum
end;
A7:
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);
( <^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 A8:
<^a,b^> <> {}
;
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;
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
;
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
;
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 A9:
fa = c
and A10:
fb = d
and A11:
<^fa,fb^> <> {}
and A12:
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 A8, Def12;
reconsider g =
g as
Morphism of
c,
d by A9, A10;
take
g
;
( a = H1(c) & b = H1(d) & <^c,d^> <> {} & f = H2(c,d,g) )
A13:
((Concretization A) . g) . [(idm c),[c,c]] = [g,[c,d]]
by A9, A10, A11, Def13;
g * (idm c) = g
by A9, A10, A11, ALTCAT_1:def 17;
then A14:
((Concretization A) . g) . [(idm c),[c,c]] = f . [(idm c),[c,c]]
by A9, A10, A12, A13;
A15:
(Concretization A) . c = a
by Def13;
(Concretization A) . d = b
by Def13;
hence
(
a = H1(
c) &
b = H1(
d) &
<^c,d^> <> {} &
f = H2(
c,
d,
g) )
by A8, A9, A10, A11, A14, A15, Th45;
verum
end;
thus
Concretization A is bijective
from YELLOW18:sch 10(A1, A2, A3, A4, A7); verum