A3: for a being Object of F₁() holds
( a is Object of F₃() iff P₁[a] ) by A2;
defpred S₁[ set , set , set ] means verum;

A4: now :: thesis: for a, b being Object of F₁()
for a9, b9 being Object of F₂() st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff S₁[a,b,f] )

let a, b be Object of F₁(); :: thesis: for a9, b9 being Object of F₂() st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff S₁[a,b,f] )
let a9, b9 be Object of F₂(); :: thesis: ( a9 = a & b9 = b & <^a,b^> <> {} implies for f being Morphism of a,b holds
( f in <^a9,b9^> iff S₁[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 S₁[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 S₁[a,b,f] ) ) ; :: thesis: verum

end;

A5: now :: thesis: for a, b being Object of F₁()
for a9, b9 being Object of F₃() st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff S₁[a,b,f] )

let a, b be Object of F₁(); :: thesis: for a9, b9 being Object of F₃() st a9 = a & b9 = b & <^a,b^> <> {} holds
for f being Morphism of a,b holds
( f in <^a9,b9^> iff S₁[a,b,f] )
let a9, b9 be Object of F₃(); :: thesis: ( a9 = a & b9 = b & <^a,b^> <> {} implies for f being Morphism of a,b holds
( f in <^a9,b9^> iff S₁[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 S₁[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 S₁[a,b,f] ) ) ; :: thesis: verum

end;

A6: for a being Object of F₁() holds
( a is Object of F₂() iff P₁[a] ) by A1;
thus 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₃() #) from YELLOW20:sch 1(A6, A4, A3, A5); :: thesis: verum