let M be non empty set ; :: thesis: for V being ComplexNormSpace
for f1, f2, f3 being PartFunc of M,V holds f1 - (f2 + f3) = (f1 - f2) - f3
let V be ComplexNormSpace; :: thesis: for f1, f2, f3 being PartFunc of M,V holds f1 - (f2 + f3) = (f1 - f2) - f3
let f1, f2, f3 be PartFunc of M,V; :: thesis: f1 - (f2 + f3) = (f1 - f2) - f3
A1: dom (f1 - (f2 + f3)) = (dom f1) /\ (dom (f2 + f3)) by VFUNCT_1:def 2
.= (dom f1) /\ ((dom f2) /\ (dom f3)) by VFUNCT_1:def 1
.= ((dom f1) /\ (dom f2)) /\ (dom f3) by XBOOLE_1:16
.= (dom (f1 - f2)) /\ (dom f3) by VFUNCT_1:def 2
.= dom ((f1 - f2) - f3) by VFUNCT_1:def 2 ;

now :: thesis: for x being Element of M st x in dom (f1 - (f2 + f3)) holds
(f1 - (f2 + f3)) /. x = ((f1 - f2) - f3) /. x

let x be Element of M; :: thesis: ( x in dom (f1 - (f2 + f3)) implies (f1 - (f2 + f3)) /. x = ((f1 - f2) - f3) /. x )
assume A2: x in dom (f1 - (f2 + f3)) ; :: thesis: (f1 - (f2 + f3)) /. x = ((f1 - f2) - f3) /. x
then x in (dom f1) /\ (dom (f2 + f3)) by VFUNCT_1:def 2;
then A3: x in dom (f2 + f3) by XBOOLE_0:def 4;
x in (dom (f1 - f2)) /\ (dom f3) by A1, A2, VFUNCT_1:def 2;
then A4: x in dom (f1 - f2) by XBOOLE_0:def 4;
thus (f1 - (f2 + f3)) /. x = (f1 /. x) - ((f2 + f3) /. x) by A2, VFUNCT_1:def 2
.= (f1 /. x) - ((f2 /. x) + (f3 /. x)) by A3, VFUNCT_1:def 1
.= ((f1 /. x) - (f2 /. x)) - (f3 /. x) by RLVECT_1:27
.= ((f1 - f2) /. x) - (f3 /. x) by A4, VFUNCT_1:def 2
.= ((f1 - f2) - f3) /. x by A1, A2, VFUNCT_1:def 2 ; :: thesis: verum

end;

hence f1 - (f2 + f3) = (f1 - f2) - f3 by A1, PARTFUN2:1; :: thesis: verum