let r be Real; :: thesis: for Fr1, Fr2 being XFinSequence of REAL st dom Fr1 = dom Fr2 & ( for n being Nat st n in len Fr1 holds
Fr1 . n = r * (Fr2 . n) ) holds
Sum Fr1 = r * (Sum Fr2)
let Fr1, Fr2 be XFinSequence of REAL ; :: thesis: ( dom Fr1 = dom Fr2 & ( for n being Nat st n in len Fr1 holds
Fr1 . n = r * (Fr2 . n) ) implies Sum Fr1 = r * (Sum Fr2) )
assume that
A1: dom Fr1 = dom Fr2 and
A2: for n being Nat st n in len Fr1 holds
Fr1 . n = r * (Fr2 . n) ; :: thesis: Sum Fr1 = r * (Sum Fr2)
A3: ( Fr1 | (dom Fr1) = Fr1 & Fr2 | (dom Fr1) = Fr2 ) by A1;
defpred S₁[ Nat] means ( $1 <= len Fr1 implies Sum (Fr1 | $1) = r * (Sum (Fr2 | $1)) );
A4: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A5: S₁[i] ; :: thesis: S₁[i + 1]
assume A6: i + 1 <= len Fr1 ; :: thesis: Sum (Fr1 | (i + 1)) = r * (Sum (Fr2 | (i + 1)))
then i < len Fr1 by NAT_1:13;
then A7: i in len Fr1 by AFINSQ_1:86;
then A8: Fr1 . i = r * (Fr2 . i) by A2;
( Sum (Fr1 | (i + 1)) = (Fr1 . i) + (Sum (Fr1 | i)) & Sum (Fr2 | (i + 1)) = (Fr2 . i) + (Sum (Fr2 | i)) ) by A1, A7, AFINSQ_2:65;
hence Sum (Fr1 | (i + 1)) = r * (Sum (Fr2 | (i + 1))) by A5, A6, A8, NAT_1:13; :: thesis: verum

end;

A9: S₁[ 0 ] ;
for i being Nat holds S₁[i] from NAT_1:sch 2(A9, A4);
hence Sum Fr1 = r * (Sum Fr2) by A3; :: thesis: verum