defpred S_{1}[ 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_{1}[x,y] )

A5: for x being object st x in [: the carrier of F,(n -tuples_on the carrier of F):] holds

S_{1}[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

( $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

proof

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
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_{1}[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_{1}[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_{1}[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_{1}[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;( y in n -tuples_on the carrier of F & S

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

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

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

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

A5: for x being object st x in [: the carrier of F,(n -tuples_on the carrier of F):] holds

S

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