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₁[ set , set ] means ( ( not $1 in i implies $2 = 1 ) & ( $1 in i implies $2 = 0 ) );
set F = Base_FinSeq n,i;
A3: 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
A4: for x being set st x in NAT holds
S₁[x,f0 . x] from FUNCT_2:sch 1(A3);
A5: len (Base_FinSeq n,i) = n by MATRIXR2:74;
A6: 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 that
0 <> n2 and
A7: n2 < len (Base_FinSeq n,i) ; :: thesis: f0 . (n2 + 1) = addreal . (f0 . n2),((Base_FinSeq n,i) . (n2 + 1))
A8: n2 + 1 <= n by A5, A7, NAT_1:13;

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

suppose A9: 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 i by NAT_1:45;
then A10: f0 . n2 = 0 by A4;
A11: 1 <= n2 + 1 by NAT_1:11;
A12: n2 + 1 in i by A9, NAT_1:45;
n2 + 1 <= len (Base_FinSeq n,i) by A7, NAT_1:13;
then addreal . (f0 . n2),((Base_FinSeq n,i) . (n2 + 1)) = addreal . 0 ,0 by A5, A9, A10, A11, MATRIXR2:76
.= 0 + 0 by BINOP_2:def 9 ;
hence f0 . (n2 + 1) = addreal . (f0 . n2),((Base_FinSeq n,i) . (n2 + 1)) by A4, A12; :: thesis: verum

end;

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

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

then i <= n2 by NAT_1:13;
then A15: not n2 in i by NAT_1:45;
A16: not n2 + 1 in i by A14, NAT_1:45;
1 <= n2 + 1 by A1, A14, XXREAL_0:2;
then (Base_FinSeq n,i) . (n2 + 1) = 0 by A8, A14, MATRIXR2:76;
then addreal . (f0 . n2),((Base_FinSeq n,i) . (n2 + 1)) = addreal . 1,0 by A4, A15
.= 1 + 0 by BINOP_2:def 9 ;
hence f0 . (n2 + 1) = addreal . (f0 . n2),((Base_FinSeq n,i) . (n2 + 1)) by A4, A16; :: thesis: verum

end;

suppose A17: 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 A17, NAT_1:45;
then f0 . n2 = 0 by A4;
then A18: addreal . (f0 . n2),((Base_FinSeq n,i) . (n2 + 1)) = addreal . 0 ,1 by A1, A2, A17, MATRIXR2:75
.= 0 + 1 by BINOP_2:def 9 ;
not n2 + 1 in i by A17;
hence f0 . (n2 + 1) = addreal . (f0 . n2),((Base_FinSeq n,i) . (n2 + 1)) by A4, A18; :: thesis: verum

end;

end;

end;

end;

end;

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

proof

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

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

then 1 in i by NAT_1:45;
then A21: f0 . 1 = 0 by A4;
1 <= n by A1, A2, XXREAL_0:2;
hence f0 . 1 = (Base_FinSeq n,i) . 1 by A20, A21, MATRIXR2:76; :: thesis: verum

end;

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

then not 1 in i by NAT_1:45;
then A23: f0 . 1 = 1 by A4;
1 = i by A1, A22, XXREAL_0:1;
hence f0 . 1 = (Base_FinSeq n,i) . 1 by A2, A23, MATRIXR2:75; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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