set ZA = the carrier of (SubstLatt V,C);
defpred S₁[ set , set , set ] means for u', v' being Element of SubstitutionSet V,C st u' = $1 & v' = $2 holds
$3 = mi (u' =>> v');
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 x' = x, y' = y as Element of SubstitutionSet V,C by SUBSTLAT:def 4;
reconsider z = mi (x' =>> y') as Element of the carrier of (SubstLatt V,C) by SUBSTLAT:def 4;
take z ; :: thesis: S₁[x,y,z]
let u', v' be Element of SubstitutionSet V,C; :: thesis: ( u' = x & v' = y implies z = mi (u' =>> v') )
assume that
A5: u' = x and
A6: v' = y ; :: thesis: z = mi (u' =>> v')
thus z = mi (u' =>> v') 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 holds S₁[a,b,o . a,b] from BINOP_1:sch 3(A4);
take o ; :: thesis: for u, v being Element of
for u', v' being Element of SubstitutionSet V,C st u' = u & v' = v holds
o . u,v = mi (u' =>> v')
let u, v be Element of ; :: thesis: for u', v' being Element of SubstitutionSet V,C st u' = u & v' = v holds
o . u,v = mi (u' =>> v')
let u', v' be Element of SubstitutionSet V,C; :: thesis: ( u' = u & v' = v implies o . u,v = mi (u' =>> v') )
assume that
A8: u' = u and
A9: v' = v ; :: thesis: o . u,v = mi (u' =>> v')
thus o . u,v = mi (u' =>> v') by A7, A8, A9; :: thesis: verum