A3:
for a being object of F1() holds
( a is object of F2() iff P1[a] )
by A1;
A4:
for a being object of F1() holds
( a is object of F3() iff P1[a] )
by A2;
defpred S1[ set , set , set ] means verum;
A5:
now let a,
b be
object of
F1();
:: thesis: for a', b' being object of F2() st a' = a & b' = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a',b'^> iff S1[a,b,f] )let a',
b' be
object of
F2();
:: thesis: ( a' = a & b' = b & <^a,b^> <> {} implies for f being Morphism of a,b holds
( f in <^a',b'^> iff S1[a,b,f] ) )assume
(
a' = a &
b' = b )
;
:: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds
( f in <^a',b'^> iff S1[a,b,f] ) )then
<^a',b'^> = <^a,b^>
by Th27;
hence
(
<^a,b^> <> {} implies for
f being
Morphism of
a,
b holds
(
f in <^a',b'^> iff
S1[
a,
b,
f] ) )
;
:: thesis: verum end;
A6:
now let a,
b be
object of
F1();
:: thesis: for a', b' being object of F3() st a' = a & b' = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a',b'^> iff S1[a,b,f] )let a',
b' be
object of
F3();
:: thesis: ( a' = a & b' = b & <^a,b^> <> {} implies for f being Morphism of a,b holds
( f in <^a',b'^> iff S1[a,b,f] ) )assume
(
a' = a &
b' = b )
;
:: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds
( f in <^a',b'^> iff S1[a,b,f] ) )then
<^a',b'^> = <^a,b^>
by Th27;
hence
(
<^a,b^> <> {} implies for
f being
Morphism of
a,
b holds
(
f in <^a',b'^> iff
S1[
a,
b,
f] ) )
;
:: thesis: verum end;
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(A3, A5, A4, A6); :: thesis: verum