defpred S1[ set , set ] 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 set st x in [:the carrier of F,(n -tuples_on the carrier of F):] holds
ex y being set st
( y in n -tuples_on the carrier of F & S1[x,y] )
proof
let x be
set ;
:: thesis: ( x in [:the carrier of F,(n -tuples_on the carrier of F):] implies ex y being set 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 set st
( y in n -tuples_on the carrier of F & S1[x,y] )
then consider x1,
v being
set such that A2:
(
x1 in the
carrier of
F &
v in n -tuples_on the
carrier of
F &
[x1,v] = x )
by ZFMISC_1:103;
reconsider x1 =
x1 as
Element of
F by A2;
reconsider v =
v as
Element of
n -tuples_on the
carrier 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:141;
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 A2;
:: 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
A3:
for x being set 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
; :: 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:106;
then consider x1 being Element of F, v1 being Element of n -tuples_on the carrier of F such that
A4:
( [x,v] = [x1,v1] & f . [x,v] = the multF of F [;] x1,v1 )
by A3;
( x1 = x & v1 = v )
by A4, ZFMISC_1:33;
hence
f . x,v = the multF of F [;] x,v
by A4; :: thesis: verum