let X be non empty set ; :: thesis: for Y being set
for f, g being PartFunc of X,REAL st Y c= dom (f + g) holds
( dom ((f + g) | Y) = Y & dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) )
let Y be set ; :: thesis: for f, g being PartFunc of X,REAL st Y c= dom (f + g) holds
( dom ((f + g) | Y) = Y & dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) )
let f, g be PartFunc of X,REAL; :: thesis: ( Y c= dom (f + g) implies ( dom ((f + g) | Y) = Y & dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) ) )
assume A1: Y c= dom (f + g) ; :: thesis: ( dom ((f + g) | Y) = Y & dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) )
(dom (f | Y)) /\ (dom (g | Y)) = ((dom f) /\ Y) /\ (dom (g | Y)) by RELAT_1:61
.= ((dom f) /\ Y) /\ ((dom g) /\ Y) by RELAT_1:61
.= (((dom f) /\ Y) /\ (dom g)) /\ Y by XBOOLE_1:16
.= (((dom f) /\ (dom g)) /\ Y) /\ Y by XBOOLE_1:16
.= ((dom f) /\ (dom g)) /\ (Y /\ Y) by XBOOLE_1:16 ;
then A2: dom ((f | Y) + (g | Y)) = ((dom f) /\ (dom g)) /\ Y by VALUED_1:def 1
.= (dom (f + g)) /\ Y by VALUED_1:def 1
.= Y by A1, XBOOLE_1:28 ;
A3: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def 1;
dom (g | Y) = (dom g) /\ Y by RELAT_1:61;
then A4: dom (g | Y) = Y by A1, A3, XBOOLE_1:18, XBOOLE_1:28;
A5: dom ((f + g) | Y) = (dom (f + g)) /\ Y by RELAT_1:61;
then A6: dom ((f + g) | Y) = Y by A1, XBOOLE_1:28;
dom (f | Y) = (dom f) /\ Y by RELAT_1:61;
then A7: dom (f | Y) = Y by A1, A3, XBOOLE_1:18, XBOOLE_1:28;

now :: thesis: for x being object st x in dom ((f + g) | Y) holds
((f + g) | Y) . x = ((f | Y) + (g | Y)) . x

let x be object ; :: thesis: ( x in dom ((f + g) | Y) implies ((f + g) | Y) . x = ((f | Y) + (g | Y)) . x )
assume A8: x in dom ((f + g) | Y) ; :: thesis: ((f + g) | Y) . x = ((f | Y) + (g | Y)) . x
hence ((f + g) | Y) . x = (f + g) . x by FUNCT_1:47
.= (f . x) + (g . x) by A1, A6, A8, VALUED_1:def 1
.= ((f | Y) . x) + (g . x) by A6, A7, A8, FUNCT_1:47
.= ((f | Y) . x) + ((g | Y) . x) by A6, A4, A8, FUNCT_1:47
.= ((f | Y) + (g | Y)) . x by A6, A2, A8, VALUED_1:def 1 ;
:: thesis: verum

end;

hence ( dom ((f + g) | Y) = Y & dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) ) by A1, A5, A2, FUNCT_1:2, XBOOLE_1:28; :: thesis: verum