let X be non empty set ; :: thesis: for Y being ComplexNormSpace
for f being Function of X, the carrier of Y st ( for x being Element of X holds f . x = 0. Y ) holds
f is bounded
let Y be ComplexNormSpace; :: thesis: for f being Function of X, the carrier of Y st ( for x being Element of X holds f . x = 0. Y ) holds
f is bounded
let f be Function of X, the carrier of Y; :: thesis: ( ( for x being Element of X holds f . x = 0. Y ) implies f is bounded )
assume A1: for x being Element of X holds f . x = 0. Y ; :: thesis: f is bounded

A2: now :: thesis: for x being Element of X holds ||.(f . x).|| = 0

let x be Element of X; :: thesis: ||.(f . x).|| = 0
thus ||.(f . x).|| = ||.(0. Y).|| by A1
.= 0 ; :: thesis: verum

end;

take 0 ; :: according to CSSPACE4:def 4 :: thesis: ( 0 <= 0 & ( for x being Element of X holds ||.(f . x).|| <= 0 ) )
thus ( 0 <= 0 & ( for x being Element of X holds ||.(f . x).|| <= 0 ) ) by A2; :: thesis: verum