let X, Y be RealLinearSpace; :: thesis: ex f being LinearOperator of Y,[:((0). X),Y:] st
( f is bijective & ( for y being Element of Y holds f . y = [(0. X),y] ) )
set A = the carrier of Y;
set B = the carrier of [:((0). X),Y:];
deffunc H₁( Element of the carrier of Y) -> Element of the carrier of [:((0). X),Y:] = In ([(0. X),$1], the carrier of [:((0). X),Y:]);
consider f being Function of the carrier of Y, the carrier of [:((0). X),Y:] such that
A1: for y being Element of the carrier of Y holds f . y = H₁(y) from FUNCT_2:sch 4();
A2: for y being Element of Y holds f . y = [(0. X),y]

proof

let y be Element of Y; :: thesis: f . y = [(0. X),y]
0. X in {(0. X)} by TARSKI:def 1;
then 0. X in the carrier of ((0). X) by RLSUB_1:def 3;
then A3: [(0. X),y] is Point of [:((0). X),Y:] by PRVECT_3:9;
thus f . y = In ([(0. X),y], the carrier of [:((0). X),Y:]) by A1
.= [(0. X),y] by A3, SUBSET_1:def 8 ; :: thesis: verum

end;

0. X in {(0. X)} by TARSKI:def 1;
then reconsider ZY = 0. X as Point of ((0). X) by RLSUB_1:def 3;
for y1, y2 being Element of Y holds f . (y1 + y2) = (f . y1) + (f . y2)

proof

let y1, y2 be Element of Y; :: thesis: f . (y1 + y2) = (f . y1) + (f . y2)
A4: f . y1 = [(0. X),y1] by A2;
A5: f . y2 = [(0. X),y2] by A2;
(f . y1) + (f . y2) = [(ZY + ZY),(y1 + y2)] by A4, A5, PRVECT_3:9
.= [((0. X) + (0. X)),(y1 + y2)] by RLSUB_1:13
.= f . (y1 + y2) by A2 ;
hence f . (y1 + y2) = (f . y1) + (f . y2) ; :: thesis: verum

end;

then A6: f is additive ;
for y being VECTOR of Y
for r being Real holds f . (r * y) = r * (f . y)

proof

let y1 be VECTOR of Y; :: thesis: for r being Real holds f . (r * y1) = r * (f . y1)
let r be Real; :: thesis: f . (r * y1) = r * (f . y1)
A7: f . y1 = [(0. X),y1] by A2;
r * (f . y1) = [(r * ZY),(r * y1)] by A7, PRVECT_3:9
.= [(r * (0. X)),(r * y1)] by RLSUB_1:14
.= [(0. X),(r * y1)] ;
hence f . (r * y1) = r * (f . y1) by A2; :: thesis: verum

end;

then reconsider f = f as LinearOperator of Y,[:((0). X),Y:] by A6, LOPBAN_1:def 5;
take f ; :: thesis: ( f is bijective & ( for y being Element of Y holds f . y = [(0. X),y] ) )

now :: thesis: for y1, y2 being object st y1 in the carrier of Y & y2 in the carrier of Y & f . y1 = f . y2 holds
y1 = y2

let y1, y2 be object ; :: thesis: ( y1 in the carrier of Y & y2 in the carrier of Y & f . y1 = f . y2 implies y1 = y2 )
assume A8: ( y1 in the carrier of Y & y2 in the carrier of Y & f . y1 = f . y2 ) ; :: thesis: y1 = y2
[(0. X),y1] = f . y1 by A2, A8
.= [(0. X),y2] by A2, A8 ;
hence y1 = y2 by XTUPLE_0:1; :: thesis: verum

end;

then A9: f is one-to-one by FUNCT_2:19;

now :: thesis: for z being object st z in the carrier of [:((0). X),Y:] holds
z in rng f

let z be object ; :: thesis: ( z in the carrier of [:((0). X),Y:] implies z in rng f )
assume z in the carrier of [:((0). X),Y:] ; :: thesis: z in rng f
then consider x being Point of ((0). X), y being Point of Y such that
A10: z = [x,y] by PRVECT_3:9;
x in the carrier of ((0). X) ;
then x in {(0. X)} by RLSUB_1:def 3;
then x = 0. X by TARSKI:def 1;
then f . y = z by A2, A10;
hence z in rng f by FUNCT_2:112; :: thesis: verum

end;

then the carrier of [:((0). X),Y:] c= rng f ;
then f is onto by FUNCT_2:def 3, XBOOLE_0:def 10;
hence ( f is bijective & ( for y being Element of Y holds f . y = [(0. X),y] ) ) by A2, A9; :: thesis: verum