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) )
A2: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def 1;
( dom ((f + g) | Y) = (dom (f + g)) /\ Y & dom (f | Y) = (dom f) /\ Y & dom (g | Y) = (dom g) /\ Y ) by RELAT_1:90;
then A3: ( dom ((f + g) | Y) = Y & dom (f | Y) = Y & dom (g | Y) = Y ) by A1, A2, XBOOLE_1:18, XBOOLE_1:28;
(dom (f | Y)) /\ (dom (g | Y)) = ((dom f) /\ Y) /\ (dom (g | Y)) by RELAT_1:90
.= ((dom f) /\ Y) /\ ((dom g) /\ Y) by RELAT_1:90
.= (((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 A4: 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 ;

now

let x be set ; :: thesis: ( x in dom ((f + g) | Y) implies ((f + g) | Y) . x = ((f | Y) + (g | Y)) . x )
assume A5: 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:70
.= (f . x) + (g . x) by A1, A3, A5, VALUED_1:def 1
.= ((f | Y) . x) + (g . x) by A3, A5, FUNCT_1:70
.= ((f | Y) . x) + ((g | Y) . x) by A3, A5, FUNCT_1:70
.= ((f | Y) + (g | Y)) . x by A3, A4, A5, 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 A3, A4, FUNCT_1:9; :: thesis: verum