defpred S1[ object , object ] means ex x1 being Element of F ex v being Element of n -tuples_on the carrier of F st
( \$1 = [x1,v] & \$2 = the multF of F [;] (x1,v) );
A1: for x being object st x in [: the carrier of F,(n -tuples_on the carrier of F):] holds
ex y being object st
( y in n -tuples_on the carrier of F & S1[x,y] )
proof
let x be object ; :: thesis: ( x in [: the carrier of F,(n -tuples_on the carrier of F):] implies ex y being object st
( y in n -tuples_on the carrier of F & S1[x,y] ) )

assume x in [: the carrier of F,(n -tuples_on the carrier of F):] ; :: thesis: ex y being object st
( y in n -tuples_on the carrier of F & S1[x,y] )

then consider x1, v being object such that
A2: x1 in the carrier of F and
A3: v in n -tuples_on the carrier of F and
A4: [x1,v] = x by ZFMISC_1:84;
reconsider v = v as Element of n -tuples_on the carrier of F by A3;
reconsider x1 = x1 as Element of F by A2;
take y = the multF of F [;] (x1,v); :: thesis: ( y in n -tuples_on the carrier of F & S1[x,y] )
y is Element of n -tuples_on the carrier of F by FINSEQ_2:121;
hence y in n -tuples_on the carrier of F ; :: thesis: S1[x,y]
take x1 ; :: thesis: ex v being Element of n -tuples_on the carrier of F st
( x = [x1,v] & y = the multF of F [;] (x1,v) )

take v ; :: thesis: ( x = [x1,v] & y = the multF of F [;] (x1,v) )
thus ( x = [x1,v] & y = the multF of F [;] (x1,v) ) by A4; :: thesis: verum
end;
consider f being Function of [: the carrier of F,(n -tuples_on the carrier of F):],(n -tuples_on the carrier of F) such that
A5: for x being object st x in [: the carrier of F,(n -tuples_on the carrier of F):] holds
S1[x,f . x] from take f ; :: thesis: for x being Element of F
for v being Element of n -tuples_on the carrier of F holds f . (x,v) = the multF of F [;] (x,v)

let x be Element of F; :: thesis: for v being Element of n -tuples_on the carrier of F holds f . (x,v) = the multF of F [;] (x,v)
let v be Element of n -tuples_on the carrier of F; :: thesis: f . (x,v) = the multF of F [;] (x,v)
[x,v] in [: the carrier of F,(n -tuples_on the carrier of F):] by ZFMISC_1:87;
then consider x1 being Element of F, v1 being Element of n -tuples_on the carrier of F such that
A6: [x,v] = [x1,v1] and
A7: f . [x,v] = the multF of F [;] (x1,v1) by A5;
x1 = x by ;
hence f . (x,v) = the multF of F [;] (x,v) by ; :: thesis: verum