defpred S₁[ object , object , object ] means ex a being Element of R ex w, u being Element of n -tuples_on the carrier of R st
( w = $3 & u = $2 & a = $1 & w = a * u );
A0: for a, x being object st a in the carrier of R & x in n -tuples_on the carrier of R holds
ex z being object st
( z in n -tuples_on the carrier of R & S₁[a,x,z] )

proof

let a1, x be object ; :: thesis: ( a1 in the carrier of R & x in n -tuples_on the carrier of R implies ex z being object st
( z in n -tuples_on the carrier of R & S₁[a1,x,z] ) )
assume AS: ( a1 in the carrier of R & x in n -tuples_on the carrier of R ) ; :: thesis: ex z being object st
( z in n -tuples_on the carrier of R & S₁[a1,x,z] )
then reconsider u = x as Tuple of n, the carrier of R by FINSEQ_2:131;
reconsider a = a1 as Element of R by AS;
take z = a * u; :: thesis: ( z in n -tuples_on the carrier of R & S₁[a1,x,z] )
thus z in n -tuples_on the carrier of R by FINSEQ_2:131; :: thesis: S₁[a1,x,z]
ex a1 being Element of R ex w1, u1 being Element of n -tuples_on the carrier of R st
( w1 = z & u1 = x & a1 = a & w1 = a1 * u1 )

proof

reconsider w = z, u = u as Element of n -tuples_on the carrier of R by FINSEQ_2:131;
take a ; :: thesis: ex w1, u1 being Element of n -tuples_on the carrier of R st
( w1 = z & u1 = x & a = a & w1 = a * u1 )
take w ; :: thesis: ex u1 being Element of n -tuples_on the carrier of R st
( w = z & u1 = x & a = a & w = a * u1 )
take u ; :: thesis: ( w = z & u = x & a = a & w = a * u )
thus ( w = z & u = x & a = a & w = a * u ) ; :: thesis: verum

end;

hence S₁[a1,x,z] ; :: thesis: verum

end;

consider f being Function of [: the carrier of R,(n -tuples_on the carrier of R):],(n -tuples_on the carrier of R) such that
A1: for x, y being object st x in the carrier of R & y in n -tuples_on the carrier of R holds
S₁[x,y,f . (x,y)] from BINOP_1:sch 1(A0);
take f ; :: thesis: for a being Element of R
for u being Tuple of n, the carrier of R holds f . (a,u) = a * u

now :: thesis: for a being Element of R
for u being Tuple of n, the carrier of R holds f . (a,u) = a * u

let a be Element of R; :: thesis: for u being Tuple of n, the carrier of R holds f . (a,u) = a * u
let u be Tuple of n, the carrier of R; :: thesis: f . (a,u) = a * u
S₁[a,u,f . (a,u)] by A1, FINSEQ_2:131;
hence f . (a,u) = a * u ; :: thesis: verum

end;

hence for a being Element of R
for u being Tuple of n, the carrier of R holds f . (a,u) = a * u ; :: thesis: verum