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

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

end;

hence ( dom ((f | Y) + (g | Y)) = Y & (f + g) | Y = (f | Y) + (g | Y) ) by A4, A1, FUNCT_1:9, RELAT_1:91; :: thesis: verum