A3:
for a being Object of F_{1}() holds

( a is Object of F_{3}() iff P_{1}[a] )
by A2;

defpred S_{1}[ set , set , set ] means verum;

_{1}() holds

( a is Object of F_{2}() iff P_{1}[a] )
by A1;

thus AltCatStr(# the carrier of F_{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}() #)
from YELLOW20:sch 1(A6, A4, A3, A5); :: thesis: verum

( a is Object of F

defpred S

A4: now :: thesis: for a, b being Object of F_{1}()

for a9, b9 being Object of F_{2}() st a9 = a & b9 = b & <^a,b^> <> {} holds

for f being Morphism of a,b holds

( f in <^a9,b9^> iff S_{1}[a,b,f] )

for a9, b9 being Object of F

for f being Morphism of a,b holds

( f in <^a9,b9^> iff S

let a, b be Object of F_{1}(); :: thesis: for a9, b9 being Object of F_{2}() st a9 = a & b9 = b & <^a,b^> <> {} holds

for f being Morphism of a,b holds

( f in <^a9,b9^> iff S_{1}[a,b,f] )

let a9, b9 be Object of F_{2}(); :: thesis: ( a9 = a & b9 = b & <^a,b^> <> {} implies for f being Morphism of a,b holds

( f in <^a9,b9^> iff S_{1}[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_{1}[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_{1}[a,b,f] ) )
; :: thesis: verum

end;for f being Morphism of a,b holds

( f in <^a9,b9^> iff S

let a9, b9 be Object of F

( f in <^a9,b9^> iff S

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

( f in <^a9,b9^> iff S

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

A5: now :: thesis: for a, b being Object of F_{1}()

for a9, b9 being Object of F_{3}() st a9 = a & b9 = b & <^a,b^> <> {} holds

for f being Morphism of a,b holds

( f in <^a9,b9^> iff S_{1}[a,b,f] )

A6:
for a being Object of Ffor a9, b9 being Object of F

for f being Morphism of a,b holds

( f in <^a9,b9^> iff S

let a, b be Object of F_{1}(); :: thesis: for a9, b9 being Object of F_{3}() st a9 = a & b9 = b & <^a,b^> <> {} holds

for f being Morphism of a,b holds

( f in <^a9,b9^> iff S_{1}[a,b,f] )

let a9, b9 be Object of F_{3}(); :: thesis: ( a9 = a & b9 = b & <^a,b^> <> {} implies for f being Morphism of a,b holds

( f in <^a9,b9^> iff S_{1}[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_{1}[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_{1}[a,b,f] ) )
; :: thesis: verum

end;for f being Morphism of a,b holds

( f in <^a9,b9^> iff S

let a9, b9 be Object of F

( f in <^a9,b9^> iff S

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

( f in <^a9,b9^> iff S

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 is Object of F

thus AltCatStr(# the carrier of F