A3: for a being Object of F1() holds
( a is Object of F3() iff P1[a] ) by A2;
defpred S1[ set , set , set ] means verum;
A4: now :: thesis: for a, b being Object of F1()
for a9, b9 being Object of F2() st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff S1[a,b,f] )
let a, b be Object of F1(); :: thesis: for a9, b9 being Object of F2() st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff S1[a,b,f] )

let a9, b9 be Object of F2(); :: thesis: ( a9 = a & b9 = b & <^a,b^> <> {} implies for f being Morphism of a,b holds
( f in <^a9,b9^> iff S1[a,b,f] ) )

assume ( a9 = a & b9 = b ) ; :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds
( f in <^a9,b9^> iff S1[a,b,f] ) )

then <^a9,b9^> = <^a,b^> by Th26;
hence ( <^a,b^> <> {} implies for f being Morphism of a,b holds
( f in <^a9,b9^> iff S1[a,b,f] ) ) ; :: thesis: verum
end;
A5: now :: thesis: for a, b being Object of F1()
for a9, b9 being Object of F3() st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff S1[a,b,f] )
let a, b be Object of F1(); :: thesis: for a9, b9 being Object of F3() st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff S1[a,b,f] )

let a9, b9 be Object of F3(); :: thesis: ( a9 = a & b9 = b & <^a,b^> <> {} implies for f being Morphism of a,b holds
( f in <^a9,b9^> iff S1[a,b,f] ) )

assume ( a9 = a & b9 = b ) ; :: thesis: ( <^a,b^> <> {} implies for f being Morphism of a,b holds
( f in <^a9,b9^> iff S1[a,b,f] ) )

then <^a9,b9^> = <^a,b^> by Th26;
hence ( <^a,b^> <> {} implies for f being Morphism of a,b holds
( f in <^a9,b9^> iff S1[a,b,f] ) ) ; :: thesis: verum
end;
A6: for a being Object of F1() holds
( a is Object of F2() iff P1[a] ) by A1;
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(A6, A4, A3, A5); :: thesis: verum