let F1, F2 be real-valued FinSequence; :: thesis: sqr (F1 + F2) = ((sqr F1) + (2 * (mlt (F1,F2)))) + (sqr F2)
A1: dom (sqr (F1 + F2)) = dom (F1 + F2) by VALUED_1:11;
A2: dom (F1 + F2) = (dom F1) /\ (dom F2) by VALUED_1:def 1;
A3: dom ((sqr F1) + (2 * (mlt (F1,F2)))) = (dom (sqr F1)) /\ (dom (2 * (mlt (F1,F2)))) by VALUED_1:def 1
.= (dom F1) /\ (dom (2 * (mlt (F1,F2)))) by VALUED_1:11
.= (dom F1) /\ (dom (mlt (F1,F2))) by VALUED_1:def 5
.= (dom F1) /\ ((dom F1) /\ (dom F2)) by VALUED_1:def 4
.= ((dom F1) /\ (dom F1)) /\ (dom F2) by XBOOLE_1:16
.= (dom F1) /\ (dom F2) ;
then A4: dom (((sqr F1) + (2 * (mlt (F1,F2)))) + (sqr F2)) = ((dom F1) /\ (dom F2)) /\ (dom (sqr F2)) by VALUED_1:def 1
.= ((dom F1) /\ (dom F2)) /\ (dom F2) by VALUED_1:11
.= (dom F1) /\ ((dom F2) /\ (dom F2)) by XBOOLE_1:16 ;

now :: thesis: for j being Nat st j in dom (sqr (F1 + F2)) holds
(sqr (F1 + F2)) . j = (((sqr F1) + (2 * (mlt (F1,F2)))) + (sqr F2)) . j

let j be Nat; :: thesis: ( j in dom (sqr (F1 + F2)) implies (sqr (F1 + F2)) . j = (((sqr F1) + (2 * (mlt (F1,F2)))) + (sqr F2)) . j )
assume A5: j in dom (sqr (F1 + F2)) ; :: thesis: (sqr (F1 + F2)) . j = (((sqr F1) + (2 * (mlt (F1,F2)))) + (sqr F2)) . j
set r1r2 = (F1 + F2) . j;
set r1 = F1 . j;
set r2 = F2 . j;
set r192 = (sqr F1) . j;
set r292 = (sqr F2) . j;
set r1r2a = (mlt (F1,F2)) . j;
set 2r1r2 = (2 * (mlt (F1,F2))) . j;
set r1922r1r2 = ((sqr F1) + (2 * (mlt (F1,F2)))) . j;
thus (sqr (F1 + F2)) . j = ((F1 + F2) . j) ^2 by VALUED_1:11
.= ((F1 . j) + (F2 . j)) ^2 by A1, A5, VALUED_1:def 1
.= (((F1 . j) ^2) + ((2 * (F1 . j)) * (F2 . j))) + ((F2 . j) ^2)
.= (((sqr F1) . j) + (2 * ((F1 . j) * (F2 . j)))) + ((F2 . j) ^2) by VALUED_1:11
.= (((sqr F1) . j) + (2 * ((F1 . j) * (F2 . j)))) + ((sqr F2) . j) by VALUED_1:11
.= (((sqr F1) . j) + (2 * ((mlt (F1,F2)) . j))) + ((sqr F2) . j) by VALUED_1:5
.= (((sqr F1) . j) + ((2 * (mlt (F1,F2))) . j)) + ((sqr F2) . j) by VALUED_1:6
.= (((sqr F1) + (2 * (mlt (F1,F2)))) . j) + ((sqr F2) . j) by A1, A2, A3, A5, VALUED_1:def 1
.= (((sqr F1) + (2 * (mlt (F1,F2)))) + (sqr F2)) . j by A1, A2, A4, A5, VALUED_1:def 1 ; :: thesis: verum

end;

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