A3:
for a being Object of F1() holds
( a is Object of F3() iff P1[a] )
by A2;
defpred S1[ set , set , set ] means verum;
A4:
now for a, b being Object of F1()
for a9, b9 being Object of F2() st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff S1[a,b,f] )let a,
b be
Object of
F1();
for a9, b9 being Object of F2() st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff S1[a,b,f] )let a9,
b9 be
Object of
F2();
( a9 = a & b9 = b & <^a,b^> <> {} implies for f being Morphism of a,b holds
( f in <^a9,b9^> iff S1[a,b,f] ) )assume
(
a9 = a &
b9 = b )
;
( <^a,b^> <> {} implies for f being Morphism of a,b holds
( f in <^a9,b9^> iff S1[a,b,f] ) )then
<^a9,b9^> = <^a,b^>
by Th26;
hence
(
<^a,b^> <> {} implies for
f being
Morphism of
a,
b holds
(
f in <^a9,b9^> iff
S1[
a,
b,
f] ) )
;
verum end;
A5:
now for a, b being Object of F1()
for a9, b9 being Object of F3() st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff S1[a,b,f] )let a,
b be
Object of
F1();
for a9, b9 being Object of F3() st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff S1[a,b,f] )let a9,
b9 be
Object of
F3();
( a9 = a & b9 = b & <^a,b^> <> {} implies for f being Morphism of a,b holds
( f in <^a9,b9^> iff S1[a,b,f] ) )assume
(
a9 = a &
b9 = b )
;
( <^a,b^> <> {} implies for f being Morphism of a,b holds
( f in <^a9,b9^> iff S1[a,b,f] ) )then
<^a9,b9^> = <^a,b^>
by Th26;
hence
(
<^a,b^> <> {} implies for
f being
Morphism of
a,
b holds
(
f in <^a9,b9^> iff
S1[
a,
b,
f] ) )
;
verum end;
A6:
for a being Object of F1() holds
( a is Object of F2() iff P1[a] )
by A1;
thus
AltCatStr(# the carrier of F2(), the Arrows of F2(), the Comp of F2() #) = AltCatStr(# the carrier of F3(), the Arrows of F3(), the Comp of F3() #)
from YELLOW20:sch 1(A6, A4, A3, A5); verum