let w1, w2 be Function of [: the carrier of R,(n -tuples_on the carrier of R):],(n -tuples_on the carrier of R); :: thesis: ( ( for a being Element of R
for u being Tuple of n, the carrier of R holds w1 . (a,u) = a * u ) & ( for a being Element of R
for u being Tuple of n, the carrier of R holds w2 . (a,u) = a * u ) implies w1 = w2 )
assume that
A1: for a being Element of R
for u being Tuple of n, the carrier of R holds w1 . (a,u) = a * u and
A2: for a being Element of R
for u being Tuple of n, the carrier of R holds w2 . (a,u) = a * u ; :: thesis: w1 = w2

now :: thesis: for o being object st o in [: the carrier of R,(n -tuples_on the carrier of R):] holds
w1 . o = w2 . o

let o be object ; :: thesis: ( o in [: the carrier of R,(n -tuples_on the carrier of R):] implies w1 . o = w2 . o )
assume o in [: the carrier of R,(n -tuples_on the carrier of R):] ; :: thesis: w1 . o = w2 . o
then consider a, u being object such that
A3: ( a in the carrier of R & u in n -tuples_on the carrier of R & o = [a,u] ) by ZFMISC_1:def 2;
reconsider a = a as Element of R by A3;
reconsider u = u as Tuple of n, the carrier of R by A3, FINSEQ_2:131;
w1 . (a,u) = a * u by A1
.= w2 . (a,u) by A2 ;
hence w1 . o = w2 . o by A3; :: thesis: verum

end;

hence w1 = w2 by FUNCT_2:12; :: thesis: verum