let X, Y be ComplexNormSpace; :: thesis:
set W = BoundedLinearOperators (X,Y);
A1: for v, u being VECTOR of () st v in BoundedLinearOperators (X,Y) & u in BoundedLinearOperators (X,Y) holds
v + u in BoundedLinearOperators (X,Y)
proof
let v, u be VECTOR of (); :: thesis: ( v in BoundedLinearOperators (X,Y) & u in BoundedLinearOperators (X,Y) implies v + u in BoundedLinearOperators (X,Y) )
assume that
A2: v in BoundedLinearOperators (X,Y) and
A3: u in BoundedLinearOperators (X,Y) ; :: thesis: v + u in BoundedLinearOperators (X,Y)
reconsider f = v + u as LinearOperator of X,Y by Def4;
f is Lipschitzian
proof
reconsider v1 = v as Lipschitzian LinearOperator of X,Y by ;
consider K2 being Real such that
A4: 0 <= K2 and
A5: for x being VECTOR of X holds ||.(v1 . x).|| <= K2 * by Def6;
reconsider u1 = u as Lipschitzian LinearOperator of X,Y by ;
consider K1 being Real such that
A6: 0 <= K1 and
A7: for x being VECTOR of X holds ||.(u1 . x).|| <= K1 * by Def6;
take K3 = K1 + K2; :: according to CLOPBAN1:def 6 :: thesis: ( 0 <= K3 & ( for x being VECTOR of X holds ||.(f . x).|| <= K3 * ) )
now :: thesis: for x being VECTOR of X holds ||.(f . x).|| <= K3 *
let x be VECTOR of X; :: thesis: ||.(f . x).|| <= K3 *
A8: ||.((u1 . x) + (v1 . x)).|| <= ||.(u1 . x).|| + ||.(v1 . x).|| by CLVECT_1:def 13;
A9: ||.(v1 . x).|| <= K2 * by A5;
||.(u1 . x).|| <= K1 * by A7;
then A10: ||.(u1 . x).|| + ||.(v1 . x).|| <= (K1 * ) + (K2 * ) by ;
||.(f . x).|| = ||.((u1 . x) + (v1 . x)).|| by Th15;
hence ||.(f . x).|| <= K3 * by ; :: thesis: verum
end;
hence ( 0 <= K3 & ( for x being VECTOR of X holds ||.(f . x).|| <= K3 * ) ) by A6, A4; :: thesis: verum
end;
hence v + u in BoundedLinearOperators (X,Y) by Def7; :: thesis: verum
end;
for c being Complex
for v being VECTOR of () st v in BoundedLinearOperators (X,Y) holds
c * v in BoundedLinearOperators (X,Y)
proof
let c be Complex; :: thesis: for v being VECTOR of () st v in BoundedLinearOperators (X,Y) holds
c * v in BoundedLinearOperators (X,Y)

let v be VECTOR of (); :: thesis: ( v in BoundedLinearOperators (X,Y) implies c * v in BoundedLinearOperators (X,Y) )
assume A11: v in BoundedLinearOperators (X,Y) ; :: thesis: c * v in BoundedLinearOperators (X,Y)
reconsider f = c * v as LinearOperator of X,Y by Def4;
f is Lipschitzian
proof
reconsider v1 = v as Lipschitzian LinearOperator of X,Y by ;
consider K being Real such that
A12: 0 <= K and
A13: for x being VECTOR of X holds ||.(v1 . x).|| <= K * by Def6;
take |.c.| * K ; :: according to CLOPBAN1:def 6 :: thesis: ( 0 <= |.c.| * K & ( for x being VECTOR of X holds ||.(f . x).|| <= (|.c.| * K) * ) )
A14: now :: thesis: for x being VECTOR of X holds ||.(f . x).|| <= (|.c.| * K) *
let x be VECTOR of X; :: thesis: ||.(f . x).|| <= (|.c.| * K) *
0 <= |.c.| by COMPLEX1:46;
then A15: |.c.| * ||.(v1 . x).|| <= |.c.| * (K * ) by ;
||.(c * (v1 . x)).|| = |.c.| * ||.(v1 . x).|| by CLVECT_1:def 13;
hence ||.(f . x).|| <= (|.c.| * K) * by ; :: thesis: verum
end;
0 <= |.c.| by COMPLEX1:46;
hence ( 0 <= |.c.| * K & ( for x being VECTOR of X holds ||.(f . x).|| <= (|.c.| * K) * ) ) by ; :: thesis: verum
end;
hence c * v in BoundedLinearOperators (X,Y) by Def7; :: thesis: verum
end;
hence BoundedLinearOperators (X,Y) is linearly-closed by ; :: thesis: verum