let K be Field; :: thesis:
let V1, V2 be VectSp of K; :: thesis:
let L be Linear_Combination of V1; :: thesis:
let F be FinSequence of V1; :: thesis:
let f be linear-transformation of V1,V2; :: thesis:
assume that
A1: f | ((Carrier L) /\ (rng F)) is one-to-one and
A2: rng F c= Carrier L ; :: thesis:
set R = rng F;
set C = Carrier L;
defpred S₁[ object , object ] means ( ( not $1 in f .: ((Carrier L) /\ (rng F)) implies $2 = 0. K ) & ( $1 in f .: ((Carrier L) /\ (rng F)) implies for v1 being Vector of V1 st v1 in (Carrier L) /\ (rng F) & f . v1 = $1 holds
$2 = L . v1 ) );
A3: for x being object st x in the carrier of V2 holds
ex y being object st
( y in the carrier of K & S₁[x,y] )

let x be object ; :: thesis:
assume x in the carrier of V2 ; :: thesis:

take 0. K ; :: thesis:
thus ( 0. K in the carrier of K & S₁[x, 0. K] ) by A4; :: thesis:

end;

then consider y being object such that
y in dom f and
A6: y in (Carrier L) /\ (rng F) and
A7: x = f . y by FUNCT_1:def 6;
reconsider y = y as Vector of V1 by A6;
take L . y ; :: thesis:

end;

hence ( L . y in the carrier of K & S₁[x,L . y] ) by A5; :: thesis:

end;

consider Lf being Function of V2,K such that
A14: for x being object st x in the carrier of V2 holds
S₁[x,Lf . x] from FUNCT_2:sch 1(A3);
reconsider Lf = Lf as Element of Funcs ( the carrier of V2, the carrier of K) by FUNCT_2:8;
for v2 being Element of V2 st not v2 in f .: ((Carrier L) /\ (rng F)) holds
Lf . v2 = 0. K by A14;
then reconsider Lf = Lf as Linear_Combination of V2 by VECTSP_6:def 1;
A15: dom f = [#] V1 by FUNCT_2:def 1;
take Lf ; :: thesis:
A16: f .: ((Carrier L) /\ (rng F)) c= Carrier Lf

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A17: y in f .: ((Carrier L) /\ (rng F)) ; :: thesis:
consider v1 being object such that
v1 in dom f and
A18: v1 in (Carrier L) /\ (rng F) and
A19: f . v1 = y by A17, FUNCT_1:def 6;
reconsider v1 = v1 as Vector of V1 by A18;
v1 in Carrier L by A18, XBOOLE_0:def 4;
then A20: L . v1 <> 0. K by VECTSP_6:2;
reconsider v2 = y as Vector of V2 by A17;
Lf . v2 = L . v1 by A14, A17, A18, A19;
hence y in Carrier Lf by A20; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A21: x in Carrier Lf ; :: thesis:
reconsider v2 = x as Vector of V2 by A21;
Lf . v2 <> 0. K by A21, VECTSP_6:2;
hence x in f .: ((Carrier L) /\ (rng F)) by A14; :: thesis:

end;

end;