A5:
the carrier of F_{2}() c= the carrier of F_{1}()
by ALTCAT_2:def 11;

A6: the carrier of F_{3}() c= the carrier of F_{1}()
by ALTCAT_2:def 11;

A7: the carrier of F_{2}() = the carrier of F_{3}()
_{2}(), the Arrows of F_{2}(), the Comp of F_{2}() #) = AltCatStr(# the carrier of F_{3}(), the Arrows of F_{3}(), the Comp of F_{3}() #)
by A7, ALTCAT_1:7, ALTCAT_2:26; :: thesis: verum

A6: the carrier of F

A7: the carrier of F

proof
_{3}() or x in the carrier of F_{2}() )

assume x in the carrier of F_{3}()
; :: thesis: x in the carrier of F_{2}()

then reconsider a = x as Object of F_{3}() ;

reconsider a = a as Object of F_{1}() by A6;

P_{1}[a]
by A3;

then a is Object of F_{2}()
by A1;

hence x in the carrier of F_{2}()
; :: thesis: verum

end;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: the carrier of F_{3}() c= the carrier of F_{2}()

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of Flet x be object ; :: thesis: ( x in the carrier of F_{2}() implies x in the carrier of F_{3}() )

assume x in the carrier of F_{2}()
; :: thesis: x in the carrier of F_{3}()

then reconsider a = x as Object of F_{2}() ;

reconsider a = a as Object of F_{1}() by A5;

P_{1}[a]
by A1;

then a is Object of F_{3}()
by A3;

hence x in the carrier of F_{3}()
; :: thesis: verum

end;assume x in the carrier of F

then reconsider a = x as Object of F

reconsider a = a as Object of F

P

then a is Object of F

hence x in the carrier of F

assume x in the carrier of F

then reconsider a = x as Object of F

reconsider a = a as Object of F

P

then a is Object of F

hence x in the carrier of F

now :: thesis: for a, b being Element of F_{2}() holds the Arrows of F_{2}() . (a,b) = the Arrows of F_{3}() . (a,b)

hence
AltCatStr(# the carrier of Flet a, b be Element of F_{2}(); :: thesis: the Arrows of F_{2}() . (a,b) = the Arrows of F_{3}() . (a,b)

reconsider x1 = a, y1 = b as Object of F_{2}() ;

reconsider x2 = x1, y2 = y1 as Object of F_{3}() by A7;

reconsider a9 = a, b9 = b as Object of F_{1}() by A5;

A8: <^x2,y2^> c= <^a9,b9^> by ALTCAT_2:31;

A9: <^x2,y2^> c= <^x1,y1^>

<^x1,y1^> c= <^x2,y2^>_{2}() . (a,b) = the Arrows of F_{3}() . (a,b)
by A9; :: thesis: verum

end;reconsider x1 = a, y1 = b as Object of F

reconsider x2 = x1, y2 = y1 as Object of F

reconsider a9 = a, b9 = b as Object of F

A8: <^x2,y2^> c= <^a9,b9^> by ALTCAT_2:31;

A9: <^x2,y2^> c= <^x1,y1^>

proof

A11:
<^x1,y1^> c= <^a9,b9^>
by ALTCAT_2:31;
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_{2}[a9,b9,f]
by A4, A8, A10;

hence f in <^x1,y1^> by A2, A8, A10; :: thesis: verum

end;assume A10: f in <^x2,y2^> ; :: thesis: f in <^x1,y1^>

then reconsider f = f as Morphism of a9,b9 by A8;

P

hence f in <^x1,y1^> by A2, A8, A10; :: thesis: verum

<^x1,y1^> c= <^x2,y2^>

proof

hence
the Arrows of F
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_{2}[a9,b9,f]
by A2, A11, A12;

hence f in <^x2,y2^> by A4, A11, A12; :: thesis: verum

end;assume A12: f in <^x1,y1^> ; :: thesis: f in <^x2,y2^>

then reconsider f = f as Morphism of a9,b9 by A11;

P

hence f in <^x2,y2^> by A4, A11, A12; :: thesis: verum