let X be non empty set ; :: thesis: for Y being ComplexNormSpace holds ComplexBoundedFunctions X,Y is linearly-closed
let Y be ComplexNormSpace; :: thesis: ComplexBoundedFunctions X,Y is linearly-closed
set W = ComplexBoundedFunctions X,Y;
A1: for v, u being VECTOR of (ComplexVectSpace X,Y) st v in ComplexBoundedFunctions X,Y & u in ComplexBoundedFunctions X,Y holds
v + u in ComplexBoundedFunctions X,Y

proof

let v, u be VECTOR of (ComplexVectSpace X,Y); :: thesis: ( v in ComplexBoundedFunctions X,Y & u in ComplexBoundedFunctions X,Y implies v + u in ComplexBoundedFunctions X,Y )
assume A2: ( v in ComplexBoundedFunctions X,Y & u in ComplexBoundedFunctions X,Y ) ; :: thesis: v + u in ComplexBoundedFunctions X,Y
reconsider f = v + u as Function of X,the carrier of Y by FUNCT_2:121;
f is bounded

proof

reconsider u1 = u as bounded Function of X,the carrier of Y by A2, Def5;
reconsider v1 = v as bounded Function of X,the carrier of Y by A2, Def5;
consider K1 being Real such that
A3: ( 0 <= K1 & ( for x being Element of X holds ||.(u1 . x).|| <= K1 ) ) by Def4;
consider K2 being Real such that
A4: ( 0 <= K2 & ( for x being Element of X holds ||.(v1 . x).|| <= K2 ) ) by Def4;
take K3 = K1 + K2; :: according to CSSPACE4:def 4 :: thesis: ( 0 <= K3 & ( for x being Element of X holds ||.(f . x).|| <= K3 ) )
A5: 0 + 0 <= K1 + K2 by A3, A4;

now

let x be Element of X; :: thesis: ||.(f . x).|| <= K3
A6: ||.(f . x).|| = ||.((v1 . x) + (u1 . x)).|| by CLOPBAN1:12;
A7: ||.((u1 . x) + (v1 . x)).|| <= ||.(u1 . x).|| + ||.(v1 . x).|| by CLVECT_1:def 11;
A8: ||.(u1 . x).|| <= K1 by A3;
||.(v1 . x).|| <= K2 by A4;
then ||.(u1 . x).|| + ||.(v1 . x).|| <= K1 + K2 by A8, XREAL_1:9;
hence ||.(f . x).|| <= K3 by A6, A7, XXREAL_0:2; :: thesis: verum

end;

hence ( 0 <= K3 & ( for x being Element of X holds ||.(f . x).|| <= K3 ) ) by A5; :: thesis: verum

end;

hence v + u in ComplexBoundedFunctions X,Y by Def5; :: thesis: verum

end;

for c being Complex
for v being VECTOR of (ComplexVectSpace X,Y) st v in ComplexBoundedFunctions X,Y holds
c * v in ComplexBoundedFunctions X,Y

proof

let c be Complex; :: thesis: for v being VECTOR of (ComplexVectSpace X,Y) st v in ComplexBoundedFunctions X,Y holds
c * v in ComplexBoundedFunctions X,Y
let v be VECTOR of (ComplexVectSpace X,Y); :: thesis: ( v in ComplexBoundedFunctions X,Y implies c * v in ComplexBoundedFunctions X,Y )
assume A9: v in ComplexBoundedFunctions X,Y ; :: thesis: c * v in ComplexBoundedFunctions X,Y
reconsider f = c * v as Function of X,the carrier of Y by FUNCT_2:121;
f is bounded

proof

reconsider v1 = v as bounded Function of X,the carrier of Y by A9, Def5;
consider K being Real such that
A10: ( 0 <= K & ( for x being Element of X holds ||.(v1 . x).|| <= K ) ) by Def4;
take K1 = |.c.| * K; :: according to CSSPACE4:def 4 :: thesis: ( 0 <= K1 & ( for x being Element of X holds ||.(f . x).|| <= K1 ) )
A11: ( 0 <= K & 0 <= |.c.| ) by A10, COMPLEX1:132;

now

let x be Element of X; :: thesis: ||.(f . x).|| <= |.c.| * K
A12: ||.(f . x).|| = ||.(c * (v1 . x)).|| by CLOPBAN1:13;
A13: ||.(c * (v1 . x)).|| = |.c.| * ||.(v1 . x).|| by CLVECT_1:def 11;
0 <= |.c.| by COMPLEX1:132;
hence ||.(f . x).|| <= |.c.| * K by A10, A12, A13, XREAL_1:66; :: thesis: verum

end;

hence ( 0 <= K1 & ( for x being Element of X holds ||.(f . x).|| <= K1 ) ) by A11; :: thesis: verum

end;

hence c * v in ComplexBoundedFunctions X,Y by Def5; :: thesis: verum

end;

hence ComplexBoundedFunctions X,Y is linearly-closed by A1, CLVECT_1:def 4; :: thesis: verum