let A1, A2 be lattice-wise category; :: thesis: ( the carrier of A1 = F₁() & ( for a, b being Object of A1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P₁[a,b,f] ) ) & the carrier of A2 = F₁() & ( for a, b being Object of A2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P₁[a,b,f] ) ) implies AltCatStr(# the carrier of A1, the Arrows of A1, the Comp of A1 #) = AltCatStr(# the carrier of A2, the Arrows of A2, the Comp of A2 #) )
deffunc H₁( set , set ) -> set = the Arrows of A1 . ($1,$2);
assume that
A1: the carrier of A1 = F₁() and
A2: for a, b being Object of A1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P₁[a,b,f] ) and
A3: the carrier of A2 = F₁() and
A4: for a, b being Object of A2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P₁[a,b,f] ) ; :: thesis: AltCatStr(# the carrier of A1, the Arrows of A1, the Comp of A1 #) = AltCatStr(# the carrier of A2, the Arrows of A2, the Comp of A2 #)

A5: now :: thesis: for a, b being Object of A2 holds <^a,b^> = the Arrows of A1 . (a,b)

let a, b be Object of A2; :: thesis: <^a,b^> = the Arrows of A1 . (a,b)
reconsider a9 = a, b9 = b as Object of A1 by A1, A3;
A6: <^a9,b9^> = the Arrows of A1 . (a9,b9) ;
thus <^a,b^> = the Arrows of A1 . (a,b) :: thesis: verum

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: the Arrows of A1 . (a,b) c= <^a,b^>

let x be object ; :: thesis: ( x in <^a,b^> implies x in the Arrows of A1 . (a,b) )
assume A7: x in <^a,b^> ; :: thesis: x in the Arrows of A1 . (a,b)
then reconsider f = x as Morphism of a,b ;
A8: @ f = f by A7, Def7;
then P₁[ latt a9, latt b9, @ f] by A4, A7;
hence x in the Arrows of A1 . (a,b) by A2, A6, A8; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the Arrows of A1 . (a,b) or x in <^a,b^> )
assume A9: x in the Arrows of A1 . (a,b) ; :: thesis: x in <^a,b^>
then reconsider f = x as Morphism of a9,b9 ;
A10: @ f = f by A9, Def7;
then P₁[ latt a, latt b, @ f] by A2, A9;
hence x in <^a,b^> by A4, A10; :: thesis: verum

end;

end;

A11: for a, b being Object of A1 holds <^a,b^> = the Arrows of A1 . (a,b) ;
for C1, C2 being semi-functional para-functional category st the carrier of C1 = F₁() & ( for a, b being Object of C1 holds <^a,b^> = H₁(a,b) ) & the carrier of C2 = F₁() & ( for a, b being Object of C2 holds <^a,b^> = H₁(a,b) ) holds
AltCatStr(# the carrier of C1, the Arrows of C1, the Comp of C1 #) = AltCatStr(# the carrier of C2, the Arrows of C2, the Comp of C2 #) from YELLOW18:sch 19();
hence AltCatStr(# the carrier of A1, the Arrows of A1, the Comp of A1 #) = AltCatStr(# the carrier of A2, the Arrows of A2, the Comp of A2 #) by A1, A3, A11, A5; :: thesis: verum