set ZA = the carrier of (SubstLatt (V,C));
defpred S₁[ 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 S₁[x,y,z]

proof

let x, y be Element of the carrier of (SubstLatt (V,C)); :: thesis: ex z being Element of the carrier of (SubstLatt (V,C)) st S₁[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 ; :: thesis: S₁[x,y,z]
let u9, v9 be Element of SubstitutionSet (V,C); :: thesis: ( u9 = x & v9 = y implies z = mi (u9 =>> v9) )
assume that
A5: u9 = x and
A6: v9 = y ; :: thesis: z = mi (u9 =>> v9)
thus z = mi (u9 =>> v9) by A5, A6; :: thesis: 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 S₁[a,b,o . (a,b)] from BINOP_1:sch 3(A4);
take o ; :: thesis: 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)); :: thesis: 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); :: thesis: ( u9 = u & v9 = v implies o . (u,v) = mi (u9 =>> v9) )
assume that
A8: u9 = u and
A9: v9 = v ; :: thesis: o . (u,v) = mi (u9 =>> v9)
thus o . (u,v) = mi (u9 =>> v9) by A7, A8, A9; :: thesis: verum