let f, g be complex-valued Function; :: thesis: for X being set holds (f + g) | X = (f | X) + (g | X)
let X be set ; :: thesis: (f + g) | X = (f | X) + (g | X)
A1: ( dom (f | X) = (dom f) /\ X & dom (g | X) = (dom g) /\ X & dom ((f + g) | X) = (dom (f + g)) /\ X ) by RELAT_1:61;
A2: ( dom (f + g) = (dom f) /\ (dom g) & dom ((f | X) + (g | X)) = (dom (f | X)) /\ (dom (g | X)) ) by VALUED_1:def 1;
then A3: dom ((f + g) | X) = ((dom f) /\ (dom g)) /\ X by RELAT_1:61
.= ((dom f) /\ X) /\ ((dom g) /\ X) by XBOOLE_1:116 ;
for x being object st x in dom ((f + g) | X) holds
((f + g) | X) . x = ((f | X) + (g | X)) . x

proof

let x be object ; :: thesis: ( x in dom ((f + g) | X) implies ((f + g) | X) . x = ((f | X) + (g | X)) . x )
assume B1: x in dom ((f + g) | X) ; :: thesis: ((f + g) | X) . x = ((f | X) + (g | X)) . x
( x in dom f & x in dom g & x in X ) by B1, A3, XBOOLE_0:def 4;
then ( x in dom (f | X) & x in dom (g | X) ) by RELAT_1:57;
then B3: ( (f | X) . x = f . x & (g | X) . x = g . x ) by FUNCT_1:47;
((f + g) | X) . x = (f + g) . x by B1, FUNCT_1:47
.= (f . x) + (g . x) by B1, A1, VALUED_1:def 1
.= ((f | X) + (g | X)) . x by B1, B3, A1, A2, A3, VALUED_1:def 1 ;
hence ((f + g) | X) . x = ((f | X) + (g | X)) . x ; :: thesis: verum

end;

hence (f + g) | X = (f | X) + (g | X) by A1, A3, VALUED_1:def 1; :: thesis: verum