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