let X be non empty set ; :: thesis: for Y being set
for f, g being PartFunc of X,COMPLEX st Y c= dom (f + g) holds
( 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,COMPLEX st Y c= dom (f + g) holds
( dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) )
let f, g be PartFunc of X,COMPLEX; :: thesis: ( Y c= dom (f + g) implies ( dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) ) )
A1: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def 1;
assume A2: Y c= dom (f + g) ; :: thesis: ( dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) )
then A3: dom ((f + g) | Y) = Y by RELAT_1:62;
dom (g | Y) = (dom g) /\ Y by RELAT_1:61;
then A4: dom (g | Y) = Y by A2, A1, XBOOLE_1:18, XBOOLE_1:28;
dom (f | Y) = (dom f) /\ Y by RELAT_1:61;
then A5: dom (f | Y) = Y by A2, A1, XBOOLE_1:18, XBOOLE_1:28;
then A6: dom ((f | Y) + (g | Y)) = Y /\ Y by A4, VALUED_1:def 1;

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 A7: 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 A2, A3, A7, VALUED_1:def 1
.= ((f | Y) . x) + (g . x) by A3, A5, A7, FUNCT_1:47
.= ((f | Y) . x) + ((g | Y) . x) by A3, A4, A7, FUNCT_1:47
.= ((f | Y) + (g | Y)) . x by A3, A6, A7, VALUED_1:def 1 ;
:: thesis: verum

end;

hence ( dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) ) by A2, A6, FUNCT_1:2, RELAT_1:62; :: thesis: verum