let m be non zero Nat; :: thesis:
let x be Element of REAL m; :: thesis:
defpred S₁[ Nat, object ] means ex ei being Element of REAL m st
( ei = (reproj ($1,(0* m))) . 1 & $2 = ((proj ($1,m)) . x) * ei );
A1: for i being Nat st i in Seg m holds
ex y being Element of REAL m st S₁[i,y]

let i be Nat; :: thesis:
assume i in Seg m ; :: thesis:
reconsider ei = (reproj (i,(0* m))) . 1 as Element of REAL m by FUNCT_2:5, NUMBERS:19;
((proj (i,m)) . x) * ei is Element of REAL m ;
hence ex y being Element of REAL m st S₁[i,y] ; :: thesis:

end;

consider s being FinSequence of REAL m such that
A2: ( dom s = Seg m & ( for i being Nat st i in Seg m holds
S₁[i,s . i] ) ) from FINSEQ_1:sch 5(A1);
take s ; :: thesis:
thus dom s = Seg m by A2; :: thesis:
m is Element of NAT by ORDINAL1:def 12;
then A3: len s = m by A2, FINSEQ_1:def 3;
thus A4: for i being Nat st 1 <= i & i <= m holds
ex ei being Element of REAL m st
( ei = (reproj (i,(0* m))) . 1 & s . i = ((proj (i,m)) . x) * ei ) :: thesis:

let i be Nat; :: thesis:
assume ( 1 <= i & i <= m ) ; :: thesis:
then i in Seg m ;
hence ex ei being Element of REAL m st
( ei = (reproj (i,(0* m))) . 1 & s . i = ((proj (i,m)) . x) * ei ) by A2; :: thesis:

end;

let i be Nat; :: thesis:
assume A7: ( 1 <= i & i <= len (Sum s) ) ; :: thesis:
then consider t being FinSequence of REAL such that
A8: ( len t = len s & ( for j being Nat st 1 <= j & j <= len s holds
ex sj being Element of REAL m st
( sj = s . j & t . j = sj . i ) ) & (Sum s) . i = Sum t ) by A5, Th4;
i in Seg m by A5, A7;
then A9: i in dom t by A3, A8, FINSEQ_1:def 3;
consider si being Element of REAL m such that
A10: ( si = s . i & t . i = si . i ) by A3, A5, A7, A8;
consider ei being Element of REAL m such that
A11: ( ei = (reproj (i,(0* m))) . 1 & s . i = ((proj (i,m)) . x) * ei ) by A4, A5, A7;
A12: (proj (i,m)) . x = x . i by PDIFF_1:def 1;
1 is Element of REAL by NUMBERS:19;
then A13: (reproj (i,(0* m))) . 1 = Replace ((0* m),i,1) by PDIFF_1:def 5;
A14: i in dom (0* m) by A5, A7;
ei . i = 1 by A11, A13, A14, FUNCT_7:31;
then A15: si . i = (x . i) * 1 by A10, A11, A12, RVSUM_1:45;
for j being Nat st j in dom t & j <> i holds
t . j = 0

let j be Nat; :: thesis:
assume A16: ( j in dom t & j <> i ) ; :: thesis:
then j in Seg (len t) by FINSEQ_1:def 3;
then A17: ( 1 <= j & j <= len s ) by A8, FINSEQ_1:1;
then consider sj being Element of REAL m such that
A18: ( sj = s . j & t . j = sj . i ) by A8;
consider ei being Element of REAL m such that
A19: ( ei = (reproj (j,(0* m))) . 1 & s . j = ((proj (j,m)) . x) * ei ) by A3, A4, A17;
1 is Element of REAL by NUMBERS:19;
then (reproj (j,(0* m))) . 1 = Replace ((0* m),j,1) by PDIFF_1:def 5;
then A20: ei . i = (0* m) . i by A16, A19, FUNCT_7:32
.= 0 ;
thus t . j = ((proj (j,m)) . x) * (ei . i) by A18, A19, RVSUM_1:45
.= 0 by A20 ; :: thesis:

end;

end;