set ZA = the carrier of (SubstLatt (V,C));
defpred S1[ set , set , set ] means for u9, v9 being Element of SubstitutionSet (V,C) st u9 = $1 & v9 = $2 holds
$3 = mi (u9 =>> v9);
A4:
for x, y being Element of the carrier of (SubstLatt (V,C)) ex z being Element of the carrier of (SubstLatt (V,C)) st S1[x,y,z]
proof
let x,
y be
Element of the
carrier of
(SubstLatt (V,C));
ex z being Element of the carrier of (SubstLatt (V,C)) st S1[x,y,z]
reconsider x9 =
x,
y9 =
y as
Element of
SubstitutionSet (
V,
C)
by SUBSTLAT:def 4;
reconsider z =
mi (x9 =>> y9) as
Element of the
carrier of
(SubstLatt (V,C)) by SUBSTLAT:def 4;
take
z
;
S1[x,y,z]
let u9,
v9 be
Element of
SubstitutionSet (
V,
C);
( u9 = x & v9 = y implies z = mi (u9 =>> v9) )
assume that A5:
u9 = x
and A6:
v9 = y
;
z = mi (u9 =>> v9)
thus
z = mi (u9 =>> v9)
by A5, A6;
verum
end;
consider o being BinOp of the carrier of (SubstLatt (V,C)) such that
A7:
for a, b being Element of (SubstLatt (V,C)) holds S1[a,b,o . (a,b)]
from BINOP_1:sch 3(A4);
take
o
; for u, v being Element of (SubstLatt (V,C))
for u9, v9 being Element of SubstitutionSet (V,C) st u9 = u & v9 = v holds
o . (u,v) = mi (u9 =>> v9)
let u, v be Element of (SubstLatt (V,C)); for u9, v9 being Element of SubstitutionSet (V,C) st u9 = u & v9 = v holds
o . (u,v) = mi (u9 =>> v9)
let u9, v9 be Element of SubstitutionSet (V,C); ( u9 = u & v9 = v implies o . (u,v) = mi (u9 =>> v9) )
assume that
A8:
u9 = u
and
A9:
v9 = v
; o . (u,v) = mi (u9 =>> v9)
thus
o . (u,v) = mi (u9 =>> v9)
by A7, A8, A9; verum