let r be real number ; :: thesis: for Fr1, Fr2 being XFinSequence of st dom Fr1 = dom Fr2 & ( for n being Element of NAT st n in len Fr1 holds
Fr1 . n = r * (Fr2 . n) ) holds
Sum Fr1 = r * (Sum Fr2)
let Fr1, Fr2 be XFinSequence of ; :: thesis: ( dom Fr1 = dom Fr2 & ( for n being Element of 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 Element of NAT st n in len Fr1 holds
Fr1 . n = r * (Fr2 . n) ; :: thesis: Sum Fr1 = r * (Sum Fr2)
defpred S₁[ Element of NAT ] means ( $1 <= len Fr1 implies Sum (Fr1 | $1) = r * (Sum (Fr2 | $1)) );
A3: S₁[ 0 ]

proof

( dom (Fr1 | 0 ) = 0 & dom (Fr2 | 0 ) = 0 ) ;
then ( Sum (Fr1 | 0 ) = 0 & Sum (Fr2 | 0 ) = 0 ) by Lm6;
hence S₁[ 0 ] ; :: thesis: verum

end;

A4: for i being Element of NAT st S₁[i] holds
S₁[i + 1]

proof

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A5: S₁[i] ; :: thesis: S₁[i + 1]
assume i + 1 <= len Fr1 ; :: thesis: Sum (Fr1 | (i + 1)) = r * (Sum (Fr2 | (i + 1)))
then i < len Fr1 by NAT_1:13;
then ( i < len Fr1 & i in len Fr1 & len Fr1 = dom Fr1 ) by NAT_1:45;
then ( Sum (Fr1 | (i + 1)) = (Fr1 . i) + (Sum (Fr1 | i)) & Sum (Fr2 | (i + 1)) = (Fr2 . i) + (Sum (Fr2 | i)) & Sum (Fr1 | i) = r * (Sum (Fr2 | i)) & Fr1 . i = r * (Fr2 . i) ) by A1, A2, A5, Lm8;
hence Sum (Fr1 | (i + 1)) = r * (Sum (Fr2 | (i + 1))) ; :: thesis: verum

end;

A6: for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A3, A4);
( len Fr1 = dom Fr1 & Fr1 | (dom Fr1) = Fr1 & Fr2 | (dom Fr1) = Fr2 ) by A1, RELAT_1:98;
hence Sum Fr1 = r * (Sum Fr2) by A6; :: thesis: verum