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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

now :: thesis: for x1, x2 being object st x1 in the carrier of X & x2 in the carrier of X & f . x1 = f . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in the carrier of X & x2 in the carrier of X & f . x1 = f . x2 implies x1 = x2 )
assume A8: ( x1 in the carrier of X & x2 in the carrier of X & f . x1 = f . x2 ) ; :: thesis: x1 = x2
[x1,(0. Y)] = f . x1 by A2, A8
.= [x2,(0. Y)] by A2, A8 ;
hence x1 = x2 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 [:X,((0). Y):] holds
z in rng f

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

end;

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