defpred S₁[ 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 & S₁[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 & S₁[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 & S₁[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 & S₁[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: S₁[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
S₁[x,f . x] from FUNCT_2:sch 1(A1);
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 A6, XTUPLE_0:1;
hence f . (x,v) = the multF of F [;] (x,v) by A6, A7, XTUPLE_0:1; :: thesis: verum