let A1, A2 be lattice-wise category; :: thesis: ( the carrier of A1 = F_{1}() & ( for a, b being Object of A1

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff P_{1}[a,b,f] ) ) & the carrier of A2 = F_{1}() & ( for a, b being Object of A2

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff P_{1}[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_{1}( set , set ) -> set = the Arrows of A1 . ($1,$2);

assume that

A1: the carrier of A1 = F_{1}()
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_{1}[a,b,f] )
and

A3: the carrier of A2 = F_{1}()
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_{1}[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 #)

for C1, C2 being semi-functional para-functional category st the carrier of C1 = F_{1}() & ( for a, b being Object of C1 holds <^a,b^> = H_{1}(a,b) ) & the carrier of C2 = F_{1}() & ( for a, b being Object of C2 holds <^a,b^> = H_{1}(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

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff P

for f being monotone Function of (latt a),(latt b) holds

( f in <^a,b^> iff P

deffunc H

assume that

A1: the carrier of A1 = F

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

A3: the carrier of A2 = F

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

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

A11:
for a, b being Object of A1 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

end;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

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_{1}[ latt a, latt b, @ f]
by A2, A9;

hence x in <^a,b^> by A4, A10; :: thesis: verum

end;

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

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the Arrows of A1 . (a,b) or x in <^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_{1}[ latt a9, latt b9, @ f]
by A4, A7;

hence x in the Arrows of A1 . (a,b) by A2, A6, A8; :: thesis: verum

end;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

hence x in the Arrows of A1 . (a,b) by A2, A6, A8; :: thesis: verum

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

hence x in <^a,b^> by A4, A10; :: thesis: verum

for C1, C2 being semi-functional para-functional category st the carrier of C1 = F

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