A5: the carrier of F₂() c= the carrier of F₁() by ALTCAT_2:def 11;
A6: the carrier of F₃() c= the carrier of F₁() by ALTCAT_2:def 11;
A7: the carrier of F₂() = the carrier of F₃()

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: the carrier of F₃() c= the carrier of F₂()

let x be object ; :: thesis: ( x in the carrier of F₂() implies x in the carrier of F₃() )
assume x in the carrier of F₂() ; :: thesis: x in the carrier of F₃()
then reconsider a = x as Object of F₂() ;
reconsider a = a as Object of F₁() by A5;
P₁[a] by A1;
then a is Object of F₃() by A3;
hence x in the carrier of F₃() ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of F₃() or x in the carrier of F₂() )
assume x in the carrier of F₃() ; :: thesis: x in the carrier of F₂()
then reconsider a = x as Object of F₃() ;
reconsider a = a as Object of F₁() by A6;
P₁[a] by A3;
then a is Object of F₂() by A1;
hence x in the carrier of F₂() ; :: thesis: verum

end;

now :: thesis: for a, b being Element of F₂() holds the Arrows of F₂() . (a,b) = the Arrows of F₃() . (a,b)

let a, b be Element of F₂(); :: thesis: the Arrows of F₂() . (a,b) = the Arrows of F₃() . (a,b)
reconsider x1 = a, y1 = b as Object of F₂() ;
reconsider x2 = x1, y2 = y1 as Object of F₃() by A7;
reconsider a9 = a, b9 = b as Object of F₁() by A5;
A8: <^x2,y2^> c= <^a9,b9^> by ALTCAT_2:31;
A9: <^x2,y2^> c= <^x1,y1^>

proof

let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in <^x2,y2^> or f in <^x1,y1^> )
assume A10: f in <^x2,y2^> ; :: thesis: f in <^x1,y1^>
then reconsider f = f as Morphism of a9,b9 by A8;
P₂[a9,b9,f] by A4, A8, A10;
hence f in <^x1,y1^> by A2, A8, A10; :: thesis: verum

end;

A11: <^x1,y1^> c= <^a9,b9^> by ALTCAT_2:31;
<^x1,y1^> c= <^x2,y2^>

proof

let f be object ; :: according to TARSKI:def 3 :: thesis: ( not f in <^x1,y1^> or f in <^x2,y2^> )
assume A12: f in <^x1,y1^> ; :: thesis: f in <^x2,y2^>
then reconsider f = f as Morphism of a9,b9 by A11;
P₂[a9,b9,f] by A2, A11, A12;
hence f in <^x2,y2^> by A4, A11, A12; :: thesis: verum

end;

hence the Arrows of F₂() . (a,b) = the Arrows of F₃() . (a,b) by A9; :: thesis: verum

end;

hence AltCatStr(# the carrier of F₂(), the Arrows of F₂(), the Comp of F₂() #) = AltCatStr(# the carrier of F₃(), the Arrows of F₃(), the Comp of F₃() #) by A7, ALTCAT_1:7, ALTCAT_2:26; :: thesis: verum