let X be non empty set ; for f, g being PartFunc of X,REAL holds
( (f + g) to_power 2 = ((f to_power 2) + (2 (#) (f (#) g))) + (g to_power 2) & (f - g) to_power 2 = ((f to_power 2) - (2 (#) (f (#) g))) + (g to_power 2) )
let f, g be PartFunc of X,REAL; ( (f + g) to_power 2 = ((f to_power 2) + (2 (#) (f (#) g))) + (g to_power 2) & (f - g) to_power 2 = ((f to_power 2) - (2 (#) (f (#) g))) + (g to_power 2) )
A1:
( dom (f to_power 2) = dom f & ( for x being Element of X st x in dom (f to_power 2) holds
(f to_power 2) . x = (f . x) to_power 2 ) )
by MESFUN6C:def 4;
A2:
( dom (g to_power 2) = dom g & ( for x being Element of X st x in dom (g to_power 2) holds
(g to_power 2) . x = (g . x) to_power 2 ) )
by MESFUN6C:def 4;
A3: dom (2 (#) (f (#) g)) =
dom (f (#) g)
by VALUED_1:def 5
.=
(dom f) /\ (dom g)
by VALUED_1:def 4
;
A5: dom ((f + g) to_power 2) =
dom (f + g)
by MESFUN6C:def 4
.=
(dom f) /\ (dom g)
by VALUED_1:def 1
;
A6: dom ((f - g) to_power 2) =
dom (f - g)
by MESFUN6C:def 4
.=
(dom f) /\ (dom g)
by VALUED_1:12
;
A7: dom ((f to_power 2) + (2 (#) (f (#) g))) =
(dom f) /\ (dom (2 (#) (f (#) g)))
by A1, VALUED_1:def 1
.=
(dom f) /\ (dom g)
by A3, XBOOLE_1:17, XBOOLE_1:28
;
A8: dom ((f to_power 2) - (2 (#) (f (#) g))) =
(dom f) /\ (dom (2 (#) (f (#) g)))
by A1, VALUED_1:12
.=
(dom f) /\ (dom g)
by A3, XBOOLE_1:17, XBOOLE_1:28
;
A9: dom (((f to_power 2) + (2 (#) (f (#) g))) + (g to_power 2)) =
(dom ((f to_power 2) + (2 (#) (f (#) g)))) /\ (dom g)
by A2, VALUED_1:def 1
.=
((dom f) /\ (dom (2 (#) (f (#) g)))) /\ (dom g)
by A1, VALUED_1:def 1
.=
((dom f) /\ (dom g)) /\ (dom g)
by A3, XBOOLE_1:17, XBOOLE_1:28
.=
(dom f) /\ (dom g)
by XBOOLE_1:17, XBOOLE_1:28
;
A10: dom (((f to_power 2) - (2 (#) (f (#) g))) + (g to_power 2)) =
(dom ((f to_power 2) - (2 (#) (f (#) g)))) /\ (dom g)
by A2, VALUED_1:def 1
.=
(dom f) /\ (dom g)
by A8, XBOOLE_1:17, XBOOLE_1:28
;
now for x being Element of X st x in (dom f) /\ (dom g) holds
( ((f + g) to_power 2) . x = (((f to_power 2) + (2 (#) (f (#) g))) + (g to_power 2)) . x & ((f - g) to_power 2) . x = (((f to_power 2) - (2 (#) (f (#) g))) + (g to_power 2)) . x )let x be
Element of
X;
( x in (dom f) /\ (dom g) implies ( ((f + g) to_power 2) . x = (((f to_power 2) + (2 (#) (f (#) g))) + (g to_power 2)) . x & ((f - g) to_power 2) . x = (((f to_power 2) - (2 (#) (f (#) g))) + (g to_power 2)) . x ) )assume A11:
x in (dom f) /\ (dom g)
;
( ((f + g) to_power 2) . x = (((f to_power 2) + (2 (#) (f (#) g))) + (g to_power 2)) . x & ((f - g) to_power 2) . x = (((f to_power 2) - (2 (#) (f (#) g))) + (g to_power 2)) . x )then A12:
x in dom (f + g)
by VALUED_1:def 1;
A13:
x in dom f
by A11, XBOOLE_0:def 4;
A14:
x in dom g
by A11, XBOOLE_0:def 4;
A15:
x in dom (f - g)
by A11, VALUED_1:12;
then A16:
x in dom ((f - g) to_power 2)
by MESFUN6C:def 4;
A17:
((f + g) to_power 2) . x =
((f + g) . x) to_power 2
by A11, A5, MESFUN6C:def 4
.=
((f . x) + (g . x)) to_power 2
by A12, VALUED_1:def 1
.=
((f . x) + (g . x)) ^2
by POWER:46
.=
(((f . x) ^2) + ((2 * (f . x)) * (g . x))) + ((g . x) ^2)
.=
(((f . x) to_power 2) + ((2 * (f . x)) * (g . x))) + ((g . x) ^2)
by POWER:46
.=
(((f . x) to_power 2) + ((2 * (f . x)) * (g . x))) + ((g . x) to_power 2)
by POWER:46
.=
(((f to_power 2) . x) + ((2 * (f . x)) * (g . x))) + ((g . x) to_power 2)
by A1, A13
.=
(((f to_power 2) . x) + ((2 * (f . x)) * (g . x))) + ((g to_power 2) . x)
by A2, A14
.=
(((f to_power 2) . x) + ((2 (#) (f (#) g)) . x)) + ((g to_power 2) . x)
by A4, A11
.=
(((f to_power 2) + (2 (#) (f (#) g))) . x) + ((g to_power 2) . x)
by A7, A11, VALUED_1:def 1
.=
(((f to_power 2) + (2 (#) (f (#) g))) + (g to_power 2)) . x
by A9, A11, VALUED_1:def 1
;
((f - g) to_power 2) . x =
((f - g) . x) to_power 2
by A16, MESFUN6C:def 4
.=
((f . x) - (g . x)) to_power 2
by A15, VALUED_1:13
.=
((f . x) - (g . x)) ^2
by POWER:46
.=
(((f . x) ^2) - ((2 * (f . x)) * (g . x))) + ((g . x) ^2)
.=
(((f . x) to_power 2) - ((2 * (f . x)) * (g . x))) + ((g . x) ^2)
by POWER:46
.=
(((f . x) to_power 2) - ((2 * (f . x)) * (g . x))) + ((g . x) to_power 2)
by POWER:46
.=
(((f to_power 2) . x) - ((2 * (f . x)) * (g . x))) + ((g . x) to_power 2)
by A1, A13
.=
(((f to_power 2) . x) - ((2 * (f . x)) * (g . x))) + ((g to_power 2) . x)
by A2, A14
.=
(((f to_power 2) . x) - ((2 (#) (f (#) g)) . x)) + ((g to_power 2) . x)
by A4, A11
.=
(((f to_power 2) - (2 (#) (f (#) g))) . x) + ((g to_power 2) . x)
by A8, A11, VALUED_1:13
.=
(((f to_power 2) - (2 (#) (f (#) g))) + (g to_power 2)) . x
by A10, A11, VALUED_1:def 1
;
hence
(
((f + g) to_power 2) . x = (((f to_power 2) + (2 (#) (f (#) g))) + (g to_power 2)) . x &
((f - g) to_power 2) . x = (((f to_power 2) - (2 (#) (f (#) g))) + (g to_power 2)) . x )
by A17;
verum end;
then
( ( for x being Element of X st x in dom ((f + g) to_power 2) holds
((f + g) to_power 2) . x = (((f to_power 2) + (2 (#) (f (#) g))) + (g to_power 2)) . x ) & ( for x being Element of X st x in dom ((f - g) to_power 2) holds
((f - g) to_power 2) . x = (((f to_power 2) - (2 (#) (f (#) g))) + (g to_power 2)) . x ) )
by A5, A6;
hence
( (f + g) to_power 2 = ((f to_power 2) + (2 (#) (f (#) g))) + (g to_power 2) & (f - g) to_power 2 = ((f to_power 2) - (2 (#) (f (#) g))) + (g to_power 2) )
by A5, A9, A10, A6, PARTFUN1:5; verum