set F = f +* (x,c);

let a be object ; :: according to VALUED_0:def 7 :: thesis: ( not a in dom (f +* (x,c)) or (f +* (x,c)) . a is complex )

assume a in dom (f +* (x,c)) ; :: thesis: (f +* (x,c)) . a is complex

let a be object ; :: according to VALUED_0:def 7 :: thesis: ( not a in dom (f +* (x,c)) or (f +* (x,c)) . a is complex )

assume a in dom (f +* (x,c)) ; :: thesis: (f +* (x,c)) . a is complex