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 A1: ( f | ((Carrier L) /\ (rng F)) is one-to-one & rng F c= Carrier L ) ; :: thesis:
set C = Carrier L;
set R = rng F;
defpred S₁[ set , set ] 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 ) );
A2: for x being set st x in the carrier of V2 holds
ex y being set st
( y in the carrier of K & S₁[x,y] )

proof

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

per cases ;

suppose A3: not x in f .: ((Carrier L) /\ (rng F)) ; :: thesis:

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

end;

suppose A4: x in f .: ((Carrier L) /\ (rng F)) ; :: thesis:

then consider y being set such that
A5: ( y in dom f & y in (Carrier L) /\ (rng F) & x = f . y ) by FUNCT_1:def 12;
reconsider y = y as Vector of V1 by A5;
take L . y ; :: thesis:

now

let v1 be Vector of V1; :: thesis:
assume A6: ( v1 in (Carrier L) /\ (rng F) & f . v1 = x ) ; :: thesis:
dom f = [#] V1 by FUNCT_2:def 1;
then ( v1 in dom (f | ((Carrier L) /\ (rng F))) & y in dom (f | ((Carrier L) /\ (rng F))) & (f | ((Carrier L) /\ (rng F))) . v1 = x & (f | ((Carrier L) /\ (rng F))) . y = x ) by A5, A6, FUNCT_1:72, RELAT_1:86;
hence L . y = L . v1 by A1, FUNCT_1:def 8; :: thesis:

end;

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

end;

consider Lf being Function of V2,K such that
A7: for x being set st x in the carrier of V2 holds
S₁[x,Lf . x] from FUNCT_2:sch 1(A2);
reconsider Lf = Lf as Element of Funcs the carrier of V2,the carrier of K by FUNCT_2:11;
for v2 being Element of V2 st not v2 in f .: ((Carrier L) /\ (rng F)) holds
Lf . v2 = 0. K by A7;
then reconsider Lf = Lf as Linear_Combination of V2 by VECTSP_6:def 4;
take Lf ; :: thesis:
A8: Carrier Lf c= f .: ((Carrier L) /\ (rng F))

proof

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

end;

f .: ((Carrier L) /\ (rng F)) c= Carrier Lf

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume A10: y in f .: ((Carrier L) /\ (rng F)) ; :: thesis:
consider v1 being set such that
A11: ( v1 in dom f & v1 in (Carrier L) /\ (rng F) & f . v1 = y ) by A10, FUNCT_1:def 12;
reconsider v1 = v1 as Vector of V1 by A11;
reconsider v2 = y as Vector of V2 by A10;
v1 in Carrier L by A11, XBOOLE_0:def 4;
then ( Lf . v2 = L . v1 & L . v1 <> 0. K ) by A7, A10, A11, VECTSP_6:20;
hence y in Carrier Lf ; :: thesis:

end;

hence Carrier Lf = f .: ((Carrier L) /\ (rng F)) by A8, XBOOLE_0:def 10; :: thesis:
A12: ( dom f = [#] V1 & rng F c= [#] V1 & rng (L (#) F) c= [#] V1 & len (L (#) F) = len F & len (Lf (#) (f * F)) = len (f * F) ) by FUNCT_2:def 1, RELAT_1:def 19, VECTSP_6:def 8;
then A13: ( dom (f * (L (#) F)) = dom (L (#) F) & dom (L (#) F) = dom F & dom (Lf (#) (f * F)) = dom (f * F) & dom (f * F) = dom F ) by FINSEQ_3:31, RELAT_1:46;

now

let x be set ; :: thesis:
assume A14: x in dom F ; :: thesis:
reconsider k = x as Nat by A14;
A15: F /. k = F . k by A14, PARTFUN1:def 8;
then A16: ( (f * F) . k = f . (F /. k) & (f * F) . k = (f * F) /. k & F . k in rng F ) by A13, A14, FUNCT_1:22, FUNCT_1:def 5, PARTFUN1:def 8;
then A17: F . k in (Carrier L) /\ (rng F) by A1, XBOOLE_0:def 4;
then (f * F) /. k in f .: ((Carrier L) /\ (rng F)) by A12, A15, A16, FUNCT_1:def 12;
then A18: L . (F /. k) = Lf . ((f * F) /. k) by A7, A15, A16, A17;
thus (f * (L (#) F)) . x = f . ((L (#) F) . k) by A13, A14, FUNCT_1:23
.= f . ((L . (F /. k)) * (F /. k)) by A13, A14, VECTSP_6:def 8
.= (Lf . ((f * F) /. k)) * ((f * F) /. k) by A16, A18, MOD_2:def 5
.= (Lf (#) (f * F)) . x by A13, A14, VECTSP_6:def 8 ; :: thesis:

end;

hence f * (L (#) F) = Lf (#) (f * F) by A13, FUNCT_1:9; :: thesis:
let v1 be Vector of V1; :: thesis:
assume A19: v1 in (Carrier L) /\ (rng F) ; :: thesis:
f . v1 in f .: ((Carrier L) /\ (rng F)) by A12, A19, FUNCT_1:def 12;
hence L . v1 = Lf . (f . v1) by A7, A19; :: thesis: