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) )
L1: ( 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 6;
L2: ( 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 6;
L3: dom (2 (#) (f (#) g)) = dom (f (#) g) by VALUED_1:def 5
.= (dom f) /\ (dom g) by VALUED_1:def 4 ;

L4: now

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;

L6: dom ((f + g) to_power 2) = dom (f + g) by MESFUN6C:def 6
.= (dom f) /\ (dom g) by VALUED_1:def 1 ;
L6M: dom ((f - g) to_power 2) = dom (f - g) by MESFUN6C:def 6
.= (dom f) /\ (dom g) by VALUED_1:12 ;
L70: dom ((f to_power 2) + (2 (#) (f (#) g))) = (dom f) /\ (dom (2 (#) (f (#) g))) by L1, VALUED_1:def 1
.= (dom f) /\ (dom g) by XBOOLE_1:17, XBOOLE_1:28, L3 ;
L70M: dom ((f to_power 2) - (2 (#) (f (#) g))) = (dom f) /\ (dom (2 (#) (f (#) g))) by L1, VALUED_1:12
.= (dom f) /\ (dom g) by XBOOLE_1:17, XBOOLE_1:28, L3 ;
L7: dom (((f to_power 2) + (2 (#) (f (#) g))) + (g to_power 2)) = (dom ((f to_power 2) + (2 (#) (f (#) g)))) /\ (dom g) by L2, VALUED_1:def 1
.= ((dom f) /\ (dom (2 (#) (f (#) g)))) /\ (dom g) by L1, VALUED_1:def 1
.= ((dom f) /\ (dom g)) /\ (dom g) by XBOOLE_1:17, XBOOLE_1:28, L3
.= (dom f) /\ (dom g) by XBOOLE_1:17, XBOOLE_1:28 ;
L7M: dom (((f to_power 2) - (2 (#) (f (#) g))) + (g to_power 2)) = (dom ((f to_power 2) - (2 (#) (f (#) g)))) /\ (dom g) by L2, VALUED_1:def 1
.= (dom f) /\ (dom g) by XBOOLE_1:17, XBOOLE_1:28, L70M ;

now

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 L81: 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 L82: x in dom (f + g) by VALUED_1:def 1;
L83: x in dom f by L81, XBOOLE_0:def 4;
L84: x in dom g by L81, XBOOLE_0:def 4;
L82M: x in dom (f - g) by VALUED_1:12, L81;
then L80M: x in dom ((f - g) to_power 2) by MESFUN6C:def 6;
H1: ((f + g) to_power 2) . x = ((f + g) . x) to_power 2 by MESFUN6C:def 6, L81, L6
.= ((f . x) + (g . x)) to_power 2 by L82, VALUED_1:def 1
.= ((f . x) + (g . x)) ^2 by POWER:53
.= (((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:53
.= (((f . x) to_power 2) + ((2 * (f . x)) * (g . x))) + ((g . x) to_power 2) by POWER:53
.= (((f to_power 2) . x) + ((2 * (f . x)) * (g . x))) + ((g . x) to_power 2) by L1, L83
.= (((f to_power 2) . x) + ((2 * (f . x)) * (g . x))) + ((g to_power 2) . x) by L2, L84
.= (((f to_power 2) . x) + ((2 (#) (f (#) g)) . x)) + ((g to_power 2) . x) by L4, L81
.= (((f to_power 2) + (2 (#) (f (#) g))) . x) + ((g to_power 2) . x) by L70, L81, VALUED_1:def 1
.= (((f to_power 2) + (2 (#) (f (#) g))) + (g to_power 2)) . x by L7, L81, VALUED_1:def 1 ;
((f - g) to_power 2) . x = ((f - g) . x) to_power 2 by MESFUN6C:def 6, L80M
.= ((f . x) - (g . x)) to_power 2 by L82M, VALUED_1:13
.= ((f . x) - (g . x)) ^2 by POWER:53
.= (((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:53
.= (((f . x) to_power 2) - ((2 * (f . x)) * (g . x))) + ((g . x) to_power 2) by POWER:53
.= (((f to_power 2) . x) - ((2 * (f . x)) * (g . x))) + ((g . x) to_power 2) by L1, L83
.= (((f to_power 2) . x) - ((2 * (f . x)) * (g . x))) + ((g to_power 2) . x) by L2, L84
.= (((f to_power 2) . x) - ((2 (#) (f (#) g)) . x)) + ((g to_power 2) . x) by L4, L81
.= (((f to_power 2) - (2 (#) (f (#) g))) . x) + ((g to_power 2) . x) by L70M, L81, VALUED_1:13
.= (((f to_power 2) - (2 (#) (f (#) g))) + (g to_power 2)) . x by L7M, L81, 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 H1; :: 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 L6, L6M;
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 PARTFUN1:34, L6, L7, L7M, L6M; :: thesis: verum