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

proof

let x be set ; :: thesis: ( x in NAT implies ex y being set st
( y in REAL & S₁[x,y] ) )
assume x in NAT ; :: thesis: ex y being set 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 set st
( y in REAL & S₁[x,y] )

then not nx in i by NAT_1:45;
hence ex y being set st
( y in REAL & S₁[x,y] ) ; :: thesis: verum

end;

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

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

end;

end;

end;

consider f0 being Function of NAT ,REAL such that
A5: for x being set st x in NAT holds
S₁[x,f0 . x] from FUNCT_2:sch 1(A4);
A6: f0 . 1 = (Base_FinSeq n,i) . 1

proof

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

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

then 1 in i by NAT_1:45;
then A8: f0 . 1 = 0 by A5;
1 <= n by A1, XXREAL_0:2;
hence f0 . 1 = (Base_FinSeq n,i) . 1 by A8, A7, MATRIXR2:76; :: thesis: verum

end;

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

then not 1 in i by NAT_1:45;
then A10: f0 . 1 = 1 by A5;
1 = i by A9, A1, XXREAL_0:1;
hence f0 . 1 = (Base_FinSeq n,i) . 1 by A10, A1, MATRIXR2:75; :: thesis: verum

end;

end;

end;

A11: 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 A1, 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 i by NAT_1:45;
hence f0 . (len (Base_FinSeq n,i)) = 1 by A5; :: thesis: verum

end;

end;

end;

for n2 being Element of 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 Element of NAT ; :: thesis: ( 0 <> n2 & n2 < len (Base_FinSeq n,i) implies f0 . (n2 + 1) = addreal . (f0 . n2),((Base_FinSeq n,i) . (n2 + 1)) )
assume A12: ( 0 <> n2 & n2 < len (Base_FinSeq n,i) ) ; :: thesis: f0 . (n2 + 1) = addreal . (f0 . n2),((Base_FinSeq n,i) . (n2 + 1))
then A13: n2 + 1 <= n by A2, NAT_1:13;

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

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

then A15: n2 + 1 in i by NAT_1:45;
n2 < i by A14, NAT_1:13;
then n2 in i by NAT_1:45;
then A16: f0 . n2 = 0 by A5;
A17: 1 <= n2 + 1 by NAT_1:11;
n2 + 1 <= len (Base_FinSeq n,i) by A12, NAT_1:13;
then addreal . (f0 . n2),((Base_FinSeq n,i) . (n2 + 1)) = addreal . 0 ,0 by A2, A14, A16, A17, MATRIXR2:76
.= 0 + 0 by BINOP_2:def 9 ;
hence f0 . (n2 + 1) = addreal . (f0 . n2),((Base_FinSeq n,i) . (n2 + 1)) by A5, A15; :: thesis: verum

end;

suppose A18: 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 A18, XXREAL_0:1;

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

then i <= n2 by NAT_1:13;
then A20: not n2 in i by NAT_1:45;
1 <= n2 + 1 by A19, A1, XXREAL_0:2;
then A21: (Base_FinSeq n,i) . (n2 + 1) = 0 by A19, A13, MATRIXR2:76;
A22: not n2 + 1 in i by A19, NAT_1:45;
addreal . (f0 . n2),((Base_FinSeq n,i) . (n2 + 1)) = addreal . 1,0 by A5, A20, A21
.= 1 + 0 by BINOP_2:def 9 ;
hence f0 . (n2 + 1) = addreal . (f0 . n2),((Base_FinSeq n,i) . (n2 + 1)) by A5, A22; :: thesis: verum

end;

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

n2 < n2 + 1 by XREAL_1:31;
then n2 in i by A23, NAT_1:45;
then f0 . n2 = 0 by A5;
then A24: addreal . (f0 . n2),((Base_FinSeq n,i) . (n2 + 1)) = addreal . 0 ,1 by A1, A23, MATRIXR2:75
.= 0 + 1 by BINOP_2:def 9 ;
not n2 + 1 in i by A23;
hence f0 . (n2 + 1) = addreal . (f0 . n2),((Base_FinSeq n,i) . (n2 + 1)) by A5, A24; :: thesis: verum

end;

end;

end;

end;

end;

hence Sum (Base_FinSeq n,i) = 1 by A3, A6, A11, FINSOP_1:def 1; :: thesis: verum