A1: dom (f | X) c= dom f by RELAT_1:60;

now :: thesis: for x being object st x in dom (f | X) holds
(f | X) . x is complex-valued Function

let x be object ; :: thesis: ( x in dom (f | X) implies (f | X) . x is complex-valued Function )
assume x in dom (f | X) ; :: thesis: (f | X) . x is complex-valued Function
then ( x in dom f & (f | X) . x = f . x ) by FUNCT_1:47, A1;
hence (f | X) . x is complex-valued Function ; :: thesis: verum

end;

hence f | X is complex-functions-valued by VALUED_2:def 26; :: thesis: verum