let F1, F2 be real-valued FinSequence; 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 for j being Nat st j in dom (sqr (F1 + F2)) holds
(sqr (F1 + F2)) . j = (((sqr F1) + (2 * (mlt (F1,F2)))) + (sqr F2)) . jlet j be
Nat;
( 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))
;
(sqr (F1 + F2)) . j = (((sqr F1) + (2 * (mlt (F1,F2)))) + (sqr F2)) . jset 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
;
verum end;
hence
sqr (F1 + F2) = ((sqr F1) + (2 * (mlt (F1,F2)))) + (sqr F2)
by A2, A4, FINSEQ_1:13, VALUED_1:11; verum