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

now

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 A2, A3, A4, A5, FINSEQ_1:17, VALUED_1:11; :: thesis: verum