let X be finite-dimensional RealNormSpace; :: thesis: for Y being RealNormSpace st dim X <> 0 holds
LinearOperators (X,Y) = BoundedLinearOperators (X,Y)
let Y be RealNormSpace; :: thesis: ( dim X <> 0 implies LinearOperators (X,Y) = BoundedLinearOperators (X,Y) )
assume A1: dim X <> 0 ; :: thesis: LinearOperators (X,Y) = BoundedLinearOperators (X,Y)
for f being object holds
( f in LinearOperators (X,Y) iff f in BoundedLinearOperators (X,Y) )

proof

let f be object ; :: thesis: ( f in LinearOperators (X,Y) iff f in BoundedLinearOperators (X,Y) )

hereby :: thesis: ( f in BoundedLinearOperators (X,Y) implies f in LinearOperators (X,Y) )

assume f in LinearOperators (X,Y) ; :: thesis: f in BoundedLinearOperators (X,Y)
then f is Lipschitzian LinearOperator of X,Y by A1, Th2, LOPBAN_1:def 6;
hence f in BoundedLinearOperators (X,Y) by LOPBAN_1:def 9; :: thesis: verum

end;

assume f in BoundedLinearOperators (X,Y) ; :: thesis: f in LinearOperators (X,Y)
then f is Lipschitzian LinearOperator of X,Y by LOPBAN_1:def 9;
hence f in LinearOperators (X,Y) by LOPBAN_1:def 6; :: thesis: verum

end;

hence LinearOperators (X,Y) = BoundedLinearOperators (X,Y) by TARSKI:2; :: thesis: verum