let f, g be complex-valued Function; :: thesis: (f - g) ^2 = (g - f) ^2
A1: dom (f - g) = (dom f) /\ (dom g) by VALUED_1:12;
A2: dom (g - f) = (dom g) /\ (dom f) by VALUED_1:12;
A3: dom ((f - g) ^2) = dom (f - g) by VALUED_1:11;
hence dom ((f - g) ^2) = dom ((g - f) ^2) by A1, A2, VALUED_1:11; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom ((f - g) ^2) or ((f - g) ^2) . b₁ = ((g - f) ^2) . b₁ )
let x be object ; :: thesis: ( not x in dom ((f - g) ^2) or ((f - g) ^2) . x = ((g - f) ^2) . x )
assume A4: x in dom ((f - g) ^2) ; :: thesis: ((f - g) ^2) . x = ((g - f) ^2) . x
then A5: (f - g) . x = (f . x) - (g . x) by A3, VALUED_1:13;
A6: (g - f) . x = (g . x) - (f . x) by A1, A3, A4, A2, VALUED_1:13;
thus ((f - g) ^2) . x = ((f - g) . x) * ((f - g) . x) by VALUED_1:5
.= ((g - f) . x) * ((g - f) . x) by A5, A6
.= ((g - f) ^2) . x by VALUED_1:5 ; :: thesis: verum