A5:
the carrier of F2() c= the carrier of F1()
by ALTCAT_2:def 11;
A6:
the carrier of F3() c= the carrier of F1()
by ALTCAT_2:def 11;
A7:
the carrier of F2() = the carrier of F3()
now for a, b being Element of F2() holds the Arrows of F2() . (a,b) = the Arrows of F3() . (a,b)let a,
b be
Element of
F2();
the Arrows of F2() . (a,b) = the Arrows of F3() . (a,b)reconsider x1 =
a,
y1 =
b as
Object of
F2() ;
reconsider x2 =
x1,
y2 =
y1 as
Object of
F3()
by A7;
reconsider a9 =
a,
b9 =
b as
Object of
F1()
by A5;
A8:
<^x2,y2^> c= <^a9,b9^>
by ALTCAT_2:31;
A9:
<^x2,y2^> c= <^x1,y1^>
proof
let f be
object ;
TARSKI:def 3 ( not f in <^x2,y2^> or f in <^x1,y1^> )
assume A10:
f in <^x2,y2^>
;
f in <^x1,y1^>
then reconsider f =
f as
Morphism of
a9,
b9 by A8;
P2[
a9,
b9,
f]
by A4, A8, A10;
hence
f in <^x1,y1^>
by A2, A8, A10;
verum
end; A11:
<^x1,y1^> c= <^a9,b9^>
by ALTCAT_2:31;
<^x1,y1^> c= <^x2,y2^>
proof
let f be
object ;
TARSKI:def 3 ( not f in <^x1,y1^> or f in <^x2,y2^> )
assume A12:
f in <^x1,y1^>
;
f in <^x2,y2^>
then reconsider f =
f as
Morphism of
a9,
b9 by A11;
P2[
a9,
b9,
f]
by A2, A11, A12;
hence
f in <^x2,y2^>
by A4, A11, A12;
verum
end; hence
the
Arrows of
F2()
. (
a,
b)
= the
Arrows of
F3()
. (
a,
b)
by A9;
verum end;
hence
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() #)
by A7, ALTCAT_1:7, ALTCAT_2:26; verum