let r be Real; :: thesis: for F being real-valued FinSequence holds sqr (r * F) = (r ^2) * (sqr F)
let F be real-valued FinSequence; :: thesis: sqr (r * F) = (r ^2) * (sqr F)
A1: dom (r * F) = dom F by VALUED_1:def 5;
A2: dom ((r ^2) * (sqr F)) = dom (sqr F) by VALUED_1:def 5;
A3: dom (sqr F) = dom F by VALUED_1:11;
now :: thesis: for i being Nat st i in dom (sqr (r * F)) holds
(sqr (r * F)) . i = ((r ^2) * (sqr F)) . i
let i be Nat; :: thesis: ( i in dom (sqr (r * F)) implies (sqr (r * F)) . i = ((r ^2) * (sqr F)) . i )
assume i in dom (sqr (r * F)) ; :: thesis: (sqr (r * F)) . i = ((r ^2) * (sqr F)) . i
thus (sqr (r * F)) . i = ((r * F) . i) ^2 by VALUED_1:11
.= (r * (F . i)) ^2 by VALUED_1:6
.= (r ^2) * ((F . i) ^2)
.= (r ^2) * ((sqr F) . i) by VALUED_1:11
.= ((r ^2) * (sqr F)) . i by VALUED_1:6 ; :: thesis: verum
end;
hence sqr (r * F) = (r ^2) * (sqr F) by A1, A2, A3, FINSEQ_1:13, VALUED_1:11; :: thesis: verum