let v be Element of INT.Ring; :: thesis: for v1 being Integer st v = v1 holds
for n being Nat holds (Nat-mult-left INT.Ring) . (n,v) = n * v1
let v1 be Integer; :: thesis: ( v = v1 implies for n being Nat holds (Nat-mult-left INT.Ring) . (n,v) = n * v1 )
assume A1: v = v1 ; :: thesis: for n being Nat holds (Nat-mult-left INT.Ring) . (n,v) = n * v1
defpred S₁[ Nat] means (Nat-mult-left INT.Ring) . ($1,v) = $1 * v1;
(Nat-mult-left INT.Ring) . (0,v) = 0. INT.Ring by BINOM:def 3
.= (0. INT.Ring) * v1 ;
then X1: S₁[ 0 ] ;
X2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume X22: S₁[n] ; :: thesis: S₁[n + 1]
(Nat-mult-left INT.Ring) . ((n + 1),v) = v + ((Nat-mult-left INT.Ring) . (n,v)) by BINOM:def 3
.= (n + 1) * v1 by A1, X22 ;
hence S₁[n + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(X1, X2);
hence for n being Nat holds (Nat-mult-left INT.Ring) . (n,v) = n * v1 ; :: thesis: verum