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

A4: now

let a, b be object of ; :: thesis: for a', b' being object of st a' = a & b' = b & <^a,b^> <> {} holds
for f being Morphism of , holds
( f in <^a',b'^> iff S₁[a,b,f] )
let a', b' be object of ; :: thesis: ( a' = a & b' = b & <^a,b^> <> {} implies for f being Morphism of , holds
( f in <^a',b'^> iff S₁[a,b,f] ) )
assume ( a' = a & b' = b ) ; :: thesis: ( <^a,b^> <> {} implies for f being Morphism of , holds
( f in <^a',b'^> iff S₁[a,b,f] ) )
then <^a',b'^> = <^a,b^> by Th27;
hence ( <^a,b^> <> {} implies for f being Morphism of , holds
( f in <^a',b'^> iff S₁[a,b,f] ) ) ; :: thesis: verum

end;

A5: now

let a, b be object of ; :: thesis: for a', b' being object of st a' = a & b' = b & <^a,b^> <> {} holds
for f being Morphism of , holds
( f in <^a',b'^> iff S₁[a,b,f] )
let a', b' be object of ; :: thesis: ( a' = a & b' = b & <^a,b^> <> {} implies for f being Morphism of , holds
( f in <^a',b'^> iff S₁[a,b,f] ) )
assume ( a' = a & b' = b ) ; :: thesis: ( <^a,b^> <> {} implies for f being Morphism of , holds
( f in <^a',b'^> iff S₁[a,b,f] ) )
then <^a',b'^> = <^a,b^> by Th27;
hence ( <^a,b^> <> {} implies for f being Morphism of , holds
( f in <^a',b'^> iff S₁[a,b,f] ) ) ; :: thesis: verum

end;

A6: for a being object of holds
( a is object of 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