let n be Nat; :: thesis: for f being n -element FinSequence of [:REAL,REAL:] ex x being Element of [:(REAL n),(REAL n):] st
for i being Nat st i in Seg n holds
( (x `1) . i = (f /. i) `1 & (x `2) . i = (f /. i) `2 )
let f be n -element FinSequence of [:REAL,REAL:]; :: thesis: ex x being Element of [:(REAL n),(REAL n):] st
for i being Nat st i in Seg n holds
( (x `1) . i = (f /. i) `1 & (x `2) . i = (f /. i) `2 )
defpred S1[ Nat, set ] means $2 = (f /. $1) `1 ;
A2: for i being Nat st i in Seg n holds
ex d being Element of REAL st S1[i,d] ;
ex x1 being FinSequence of REAL st
( len x1 = n & ( for i being Nat st i in Seg n holds
S1[i,x1 /. i] ) ) from FINSEQ_4:sch 1(A2);
 then consider x1 being FinSequence of REAL such that
A3: len x1 = n and
A4: for i being Nat st i in Seg n holds
x1 /. i = (f /. i) `1 ;
dom x1 = Seg n by A3, FINSEQ_1:def 3;
then reconsider x1 = x1 as Element of REAL n by REAL_NS1:6;
defpred S2[ Nat, set ] means $2 = (f /. $1) `2 ;
A5: for i being Nat st i in Seg n holds
ex d being Element of REAL st S2[i,d] ;
ex x2 being FinSequence of REAL st
( len x2 = n & ( for i being Nat st i in Seg n holds
S2[i,x2 /. i] ) ) from FINSEQ_4:sch 1(A5);
 then consider x2 being FinSequence of REAL such that
A6: len x2 = n and
A7: for i being Nat st i in Seg n holds
x2 /. i = (f /. i) `2 ;
dom x2 = Seg n by A6, FINSEQ_1:def 3;
then reconsider x2 = x2 as Element of REAL n by REAL_NS1:6;
reconsider x = [x1,x2] as Element of [:(REAL n),(REAL n):] by ZFMISC_1:def 2;
take x ; :: thesis: for i being Nat st i in Seg n holds
( (x `1) . i = (f /. i) `1 & (x `2) . i = (f /. i) `2 )
now :: thesis: for i being Nat st i in Seg n holds
( (x `1) . i = (f /. i) `1 & (x `2) . i = (f /. i) `2 )
let i be Nat; :: thesis: ( i in Seg n implies ( (x `1) . i = (f /. i) `1 & (x `2) . i = (f /. i) `2 ) )
assume A8: i in Seg n ; :: thesis: ( (x `1) . i = (f /. i) `1 & (x `2) . i = (f /. i) `2 )
then A9: ( x1 /. i = (f /. i) `1 & x2 /. i = (f /. i) `2 ) by A4, A7;
( i in dom x1 & i in dom x2 ) by A3, FINSEQ_1:def 3, A8, A6;
hence ( (x `1) . i = (f /. i) `1 & (x `2) . i = (f /. i) `2 ) by A9, PARTFUN1:def 6; :: thesis: verum
end;
hence for i being Nat st i in Seg n holds
( (x `1) . i = (f /. i) `1 & (x `2) . i = (f /. i) `2 ) ; :: thesis: verum