let A1, A2 be lattice-wise category; :: thesis: ( the carrier of A1 = F1() & ( for a, b being object of A1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P1[a,b,f] ) ) & the carrier of A2 = F1() & ( for a, b being object of A2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P1[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 H1( set , set ) -> set = the Arrows of A1 . $1,$2;
A1:
for C1, C2 being semi-functional para-functional category st the carrier of C1 = F1() & ( for a, b being object of C1 holds <^a,b^> = H1(a,b) ) & the carrier of C2 = F1() & ( for a, b being object of C2 holds <^a,b^> = H1(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();
assume that
A2:
the carrier of A1 = F1()
and
A3:
for a, b being object of A1
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P1[a,b,f] )
and
A4:
the carrier of A2 = F1()
and
A5:
for a, b being object of A2
for f being monotone Function of (latt a),(latt b) holds
( f in <^a,b^> iff P1[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 #)
A6:
for a, b being object of A1 holds <^a,b^> = the Arrows of A1 . a,b
;
now let a,
b be
object of
A2;
:: thesis: <^a,b^> = the Arrows of A1 . a,breconsider a' =
a,
b' =
b as
object of
A1 by A2, A4;
A7:
<^a',b'^> = the
Arrows of
A1 . a',
b'
;
thus
<^a,b^> = the
Arrows of
A1 . a,
b
:: thesis: verumproof
hereby :: according to TARSKI:def 3,
XBOOLE_0:def 10 :: thesis: the Arrows of A1 . a,b c= <^a,b^>
let x be
set ;
:: thesis: ( x in <^a,b^> implies x in the Arrows of A1 . a,b )assume A8:
x in <^a,b^>
;
:: thesis: x in the Arrows of A1 . a,bthen reconsider f =
x as
Morphism of
a,
b ;
A9:
@ f = f
by A8, Def7;
then
(
P1[
latt a',
latt b',
@ f] &
@ f is
Function of
(latt a'),
(latt b') )
by A5, A8;
hence
x in the
Arrows of
A1 . a,
b
by A3, A7, A9;
:: thesis: verum
end;
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in the Arrows of A1 . a,b or x in <^a,b^> )
assume A10:
x in the
Arrows of
A1 . a,
b
;
:: thesis: x in <^a,b^>
then reconsider f =
x as
Morphism of
a',
b' ;
@ f = f
by A10, Def7;
then
(
P1[
latt a,
latt b,
@ f] &
f = @ f )
by A3, A10;
hence
x in <^a,b^>
by A5;
:: thesis: verum
end; end;
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, A2, A4, A6; :: thesis: verum