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()
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: the carrier of F3() c= the carrier of F2()
let x be object ; :: thesis: ( x in the carrier of F2() implies x in the carrier of F3() )
assume x in the carrier of F2() ; :: thesis: x in the carrier of F3()
then reconsider a = x as Object of F2() ;
reconsider a = a as Object of F1() by A5;
P1[a] by A1;
then a is Object of F3() by A3;
hence x in the carrier of F3() ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of F3() or x in the carrier of F2() )
assume x in the carrier of F3() ; :: thesis: x in the carrier of F2()
then reconsider a = x as Object of F3() ;
reconsider a = a as Object of F1() by A6;
P1[a] by A3;
then a is Object of F2() by A1;
hence x in the carrier of F2() ; :: thesis: verum
end;
now :: thesis: 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(); :: thesis: 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 ; :: 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;
P2[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;
P2[a9,b9,f] by A2, A11, A12;
hence f in <^x2,y2^> by A4, A11, A12; :: thesis: verum
end;
hence the Arrows of F2() . (a,b) = the Arrows of F3() . (a,b) by A9; :: thesis: 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; :: thesis: verum