let V, W be RealLinearSpace; :: thesis: for X being set holds
( X is LinearOperator of V,W iff X is linear-transformation of (RLSp2RVSp V),(RLSp2RVSp W) )
let X be set ; :: thesis: ( X is LinearOperator of V,W iff X is linear-transformation of (RLSp2RVSp V),(RLSp2RVSp W) )

hereby :: thesis: ( X is linear-transformation of (RLSp2RVSp V),(RLSp2RVSp W) implies X is LinearOperator of V,W )

assume X is LinearOperator of V,W ; :: thesis: X is linear-transformation of (RLSp2RVSp V),(RLSp2RVSp W)
then reconsider T = X as LinearOperator of V,W ;
reconsider f = T as Function of (RLSp2RVSp V),(RLSp2RVSp W) ;
for x, y being Element of (RLSp2RVSp V) holds f . (x + y) = (f . x) + (f . y)

proof

let x, y be Element of (RLSp2RVSp V); :: thesis: f . (x + y) = (f . x) + (f . y)
A1: T is additive ;
reconsider x0 = x, y0 = y as Element of V ;
thus f . (x + y) = T . (x0 + y0)
.= (T . x0) + (T . y0) by A1
.= (f . x) + (f . y) ; :: thesis: verum

end;

then A2: f is additive ;
for a being Scalar of F_Real
for x being Vector of (RLSp2RVSp V) holds f . (a * x) = a * (f . x)

proof

let a be Scalar of F_Real; :: thesis: for x being Vector of (RLSp2RVSp V) holds f . (a * x) = a * (f . x)
let x be Element of (RLSp2RVSp V); :: thesis: f . (a * x) = a * (f . x)
reconsider x0 = x as Element of V ;
reconsider a0 = a as Element of REAL ;
thus f . (a * x) = T . (a0 * x0)
.= a0 * (T . x0) by LOPBAN_1:def 5
.= a * (f . x) ; :: thesis: verum

end;

hence X is linear-transformation of (RLSp2RVSp V),(RLSp2RVSp W) by MOD_2:def 2, A2; :: thesis: verum

end;

assume X is linear-transformation of (RLSp2RVSp V),(RLSp2RVSp W) ; :: thesis: X is LinearOperator of V,W
then reconsider T = X as linear-transformation of (RLSp2RVSp V),(RLSp2RVSp W) ;
reconsider f = T as Function of V,W ;
for x, y being Element of V holds f . (x + y) = (f . x) + (f . y)

proof

let x, y be Element of V; :: thesis: f . (x + y) = (f . x) + (f . y)
A3: T is additive ;
reconsider x0 = x, y0 = y as Element of (RLSp2RVSp V) ;
thus f . (x + y) = T . (x0 + y0)
.= (T . x0) + (T . y0) by A3
.= (f . x) + (f . y) ; :: thesis: verum

end;

then A4: f is additive ;
for a being Real
for x being VECTOR of V holds f . (a * x) = a * (f . x)

proof

let a be Real; :: thesis: for x being VECTOR of V holds f . (a * x) = a * (f . x)
let x be VECTOR of V; :: thesis: f . (a * x) = a * (f . x)
reconsider x0 = x as Element of (RLSp2RVSp V) ;
reconsider a0 = a as Element of F_Real by XREAL_0:def 1;
thus f . (a * x) = T . (a0 * x0)
.= a0 * (T . x0) by MOD_2:def 2
.= a * (f . x) ; :: thesis: verum

end;

then f is homogeneous ;
hence X is LinearOperator of V,W by A4; :: thesis: verum