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 ;
( 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):]
;
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);
( 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
;
S1[x,y]
take
x1
;
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
;
( x = [x1,v] & y = the multF of F [;] (x1,v) )
thus
(
x = [x1,v] &
y = the
multF of
F [;] (
x1,
v) )
by A4;
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 FUNCT_2:sch 1(A1);
take
f
; 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; 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; 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; verum