let i, n be Nat; :: thesis: ( 1 <= i & i <= n implies Sum (Base_FinSeq (n,i)) = 1 )
assume that
A1: 1 <= i and
A2: i <= n ; :: thesis: Sum (Base_FinSeq (n,i)) = 1
defpred S₁[ object , object ] means ( ( not $1 in i implies $2 = 1 ) & ( $1 in i implies $2 = 0 ) );
set F = Base_FinSeq (n,i);
A3: for x being object st x in NAT holds
ex y being object st
( y in REAL & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in NAT implies ex y being object st
( y in REAL & S₁[x,y] ) )
assume x in NAT ; :: thesis: ex y being object st
( y in REAL & S₁[x,y] )
then reconsider nx = x as Element of NAT ;

per cases ( nx >= i or nx < i ) ;

suppose nx >= i ; :: thesis: ex y being object st
( y in REAL & S₁[x,y] )

then A4: not nx in Segm i by NAT_1:44;
take y = 1; :: thesis: ( y in REAL & S₁[x,y] )
thus y in REAL by XREAL_0:def 1; :: thesis: S₁[x,y]
thus S₁[x,y] by A4; :: thesis: verum

end;

suppose nx < i ; :: thesis: ex y being object st
( y in REAL & S₁[x,y] )

then nx in Segm i by NAT_1:44;
hence ex y being object st
( y in REAL & S₁[x,y] ) by Lm3; :: thesis: verum

end;

end;

end;

consider f0 being sequence of REAL such that
A5: for x being object st x in NAT holds
S₁[x,f0 . x] from FUNCT_2:sch 1(A3);
A6: len (Base_FinSeq (n,i)) = n by MATRIXR2:74;
A7: for n2 being Nat st 0 <> n2 & n2 < len (Base_FinSeq (n,i)) holds
f0 . (n2 + 1) = addreal . ((f0 . n2),((Base_FinSeq (n,i)) . (n2 + 1)))

proof

let n2 be Nat; :: thesis: ( 0 <> n2 & n2 < len (Base_FinSeq (n,i)) implies f0 . (n2 + 1) = addreal . ((f0 . n2),((Base_FinSeq (n,i)) . (n2 + 1))) )
assume that
0 <> n2 and
A8: n2 < len (Base_FinSeq (n,i)) ; :: thesis: f0 . (n2 + 1) = addreal . ((f0 . n2),((Base_FinSeq (n,i)) . (n2 + 1)))
A9: n2 + 1 <= n by A6, A8, NAT_1:13;
A10: n2 in NAT by ORDINAL1:def 12;

per cases ( n2 + 1 < i or i <= n2 + 1 ) ;

suppose A11: n2 + 1 < i ; :: thesis: f0 . (n2 + 1) = addreal . ((f0 . n2),((Base_FinSeq (n,i)) . (n2 + 1)))

then n2 < i by NAT_1:13;
then n2 in Segm i by NAT_1:44;
then A12: f0 . n2 = 0 by A5, A10;
A13: 1 <= n2 + 1 by NAT_1:11;
A14: n2 + 1 in Segm i by A11, NAT_1:44;
n2 + 1 <= len (Base_FinSeq (n,i)) by A8, NAT_1:13;
then addreal . ((f0 . n2),((Base_FinSeq (n,i)) . (n2 + 1))) = addreal . (0,0) by A6, A11, A12, A13, MATRIXR2:76
.= 0 + 0 by BINOP_2:def 9 ;
hence f0 . (n2 + 1) = addreal . ((f0 . n2),((Base_FinSeq (n,i)) . (n2 + 1))) by A5, A14; :: thesis: verum

end;

suppose A15: i <= n2 + 1 ; :: thesis: f0 . (n2 + 1) = addreal . ((f0 . n2),((Base_FinSeq (n,i)) . (n2 + 1)))

per cases ( i < n2 + 1 or i = n2 + 1 ) by A15, XXREAL_0:1;

suppose A16: i < n2 + 1 ; :: thesis: f0 . (n2 + 1) = addreal . ((f0 . n2),((Base_FinSeq (n,i)) . (n2 + 1)))

then i <= n2 by NAT_1:13;
then A17: not n2 in Segm i by NAT_1:44;
A18: not n2 + 1 in Segm i by A16, NAT_1:44;
1 <= n2 + 1 by A1, A16, XXREAL_0:2;
then (Base_FinSeq (n,i)) . (n2 + 1) = 0 by A9, A16, MATRIXR2:76;
then addreal . ((f0 . n2),((Base_FinSeq (n,i)) . (n2 + 1))) = addreal . (1,0) by A5, A17, A10
.= 1 + 0 by BINOP_2:def 9 ;
hence f0 . (n2 + 1) = addreal . ((f0 . n2),((Base_FinSeq (n,i)) . (n2 + 1))) by A5, A18; :: thesis: verum

end;

suppose A19: i = n2 + 1 ; :: thesis: f0 . (n2 + 1) = addreal . ((f0 . n2),((Base_FinSeq (n,i)) . (n2 + 1)))

n2 < n2 + 1 by XREAL_1:29;
then n2 in Segm i by A19, NAT_1:44;
then f0 . n2 = 0 by A5, A10;
then A20: addreal . ((f0 . n2),((Base_FinSeq (n,i)) . (n2 + 1))) = addreal . (0,1) by A1, A2, A19, MATRIXR2:75
.= 0 + 1 by BINOP_2:def 9 ;
not n2 + 1 in i by A19;
hence f0 . (n2 + 1) = addreal . ((f0 . n2),((Base_FinSeq (n,i)) . (n2 + 1))) by A5, A20; :: thesis: verum

end;

end;

end;

end;

end;

A21: f0 . 1 = (Base_FinSeq (n,i)) . 1

proof

per cases ( 1 < i or 1 >= i ) ;

suppose A22: 1 < i ; :: thesis: f0 . 1 = (Base_FinSeq (n,i)) . 1

then 1 in Segm i by NAT_1:44;
then A23: f0 . 1 = 0 by A5;
1 <= n by A1, A2, XXREAL_0:2;
hence f0 . 1 = (Base_FinSeq (n,i)) . 1 by A22, A23, MATRIXR2:76; :: thesis: verum

end;

suppose A24: 1 >= i ; :: thesis: f0 . 1 = (Base_FinSeq (n,i)) . 1

then not 1 in Segm i by NAT_1:44;
then A25: f0 . 1 = 1 by A5;
1 = i by A1, A24, XXREAL_0:1;
hence f0 . 1 = (Base_FinSeq (n,i)) . 1 by A2, A25, MATRIXR2:75; :: thesis: verum

end;

end;

end;

A26: f0 . (len (Base_FinSeq (n,i))) = 1

proof

per cases ( len (Base_FinSeq (n,i)) < i or len (Base_FinSeq (n,i)) >= i ) ;

suppose len (Base_FinSeq (n,i)) < i ; :: thesis: f0 . (len (Base_FinSeq (n,i))) = 1

hence f0 . (len (Base_FinSeq (n,i))) = 1 by A2, MATRIXR2:74; :: thesis: verum

end;

suppose len (Base_FinSeq (n,i)) >= i ; :: thesis: f0 . (len (Base_FinSeq (n,i))) = 1

then not len (Base_FinSeq (n,i)) in Segm i by NAT_1:44;
hence f0 . (len (Base_FinSeq (n,i))) = 1 by A5; :: thesis: verum

end;

end;

end;

len (Base_FinSeq (n,i)) >= 1 by A1, A2, A6, XXREAL_0:2;
hence Sum (Base_FinSeq (n,i)) = 1 by A21, A26, A7, FINSOP_1:def 1; :: thesis: verum