let F1, F2 be real-valued FinSequence; :: thesis: sqr (mlt (F1,F2)) = mlt ((sqr F1),(sqr F2))
A1: dom (mlt (F1,F2)) = (dom F1) /\ (dom F2) by VALUED_1:def 4;
A2: dom (mlt ((sqr F1),(sqr F2))) = (dom (sqr F1)) /\ (dom (sqr F2)) by VALUED_1:def 4;
A3: dom (sqr F1) = dom F1 by VALUED_1:11;
A4: dom (sqr F2) = dom F2 by VALUED_1:11;

now :: thesis: for i being Nat st i in dom (sqr (mlt (F1,F2))) holds
(sqr (mlt (F1,F2))) . i = (mlt ((sqr F1),(sqr F2))) . i

let i be Nat; :: thesis: ( i in dom (sqr (mlt (F1,F2))) implies (sqr (mlt (F1,F2))) . i = (mlt ((sqr F1),(sqr F2))) . i )
assume i in dom (sqr (mlt (F1,F2))) ; :: thesis: (sqr (mlt (F1,F2))) . i = (mlt ((sqr F1),(sqr F2))) . i
thus (sqr (mlt (F1,F2))) . i = ((mlt (F1,F2)) . i) ^2 by VALUED_1:11
.= ((F1 . i) * (F2 . i)) ^2 by VALUED_1:5
.= ((F1 . i) ^2) * ((F2 . i) ^2)
.= ((sqr F1) . i) * ((F2 . i) ^2) by VALUED_1:11
.= ((sqr F1) . i) * ((sqr F2) . i) by VALUED_1:11
.= (mlt ((sqr F1),(sqr F2))) . i by VALUED_1:5 ; :: thesis: verum

end;

hence sqr (mlt (F1,F2)) = mlt ((sqr F1),(sqr F2)) by A1, A2, A3, A4, FINSEQ_1:13, VALUED_1:11; :: thesis: verum