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 )

per cases ( n is zero or not n is zero ) ;

suppose A1: n is zero ; :: 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 )

then REAL n = {(<*> REAL)} by FINSEQ_2:94;
then <*> REAL in REAL 0 by A1, TARSKI:def 1;
then reconsider x = [(<*> REAL),(<*> REAL)] as Element of [:(REAL n),(REAL n):] by A1, 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 )
thus for i being Nat st i in Seg n holds
( (x `1) . i = (f /. i) `1 & (x `2) . i = (f /. i) `2 ) by A1; :: thesis: verum

end;

suppose not n is zero ; :: 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 S₁[ 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 S<sub>1</sub>[i,d] ;
ex x1 being FinSequence of REAL st
( len x1 = n & ( for i being Nat st i in Seg n holds
S<sub>1</sub>[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 S₂[ 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 S<sub>2</sub>[i,d] ;
ex x2 being FinSequence of REAL st
( len x2 = n & ( for i being Nat st i in Seg n holds
S<sub>2</sub>[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

end;

end;