let X be non empty set ; :: thesis: 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; :: thesis: ( (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 ;

A4: now :: thesis: for x being Element of X st x in (dom f) /\ (dom g) holds
(2 (#) (f (#) g)) . x = (2 * (f . x)) * (g . x)

let x be Element of X; :: thesis: ( x in (dom f) /\ (dom g) implies (2 (#) (f (#) g)) . x = (2 * (f . x)) * (g . x) )
assume x in (dom f) /\ (dom g) ; :: thesis: (2 (#) (f (#) g)) . x = (2 * (f . x)) * (g . x)
thus (2 (#) (f (#) g)) . x = 2 * ((f (#) g) . x) by VALUED_1:6
.= 2 * ((f . x) * (g . x)) by VALUED_1:5
.= (2 * (f . x)) * (g . x) ; :: thesis: verum

end;

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 :: thesis: 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; :: thesis: ( 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) ; :: thesis: ( ((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; :: thesis: 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; :: thesis: verum