end;

let x be object ; :: thesis:
assume A13: x in Carrier L ; :: thesis:
then consider v being Vector of V such that
A14: x = v and
A15: L . v <> 0 ;
K . v <> 0 by A1, A2, A3, A13, A14, A15, FUNCT_1:47;
hence x in Carrier K by A1, A13, A14; :: thesis:

end;

then A16: Carrier L c= Carrier K ;
then A17: Carrier K = Carrier L by A7, XBOOLE_0:def 10;
F,G are_fiberwise_equipotent by A7, A8, A10, A11, A16, RFINSEQ:26, XBOOLE_0:def 10;
then consider P being Permutation of (dom G) such that
A18: F = G * P by RFINSEQ:4;
len (K (#) G) = len G by VECTSP_6:def 5;
then A19: dom (K (#) G) = dom G by FINSEQ_3:29;
then reconsider q = (K (#) G) * P as FinSequence of W by FINSEQ_2:47;
A20: len q = len (K (#) G) by A19, FINSEQ_2:44;
then len q = len G by VECTSP_6:def 5;
then A21: dom q = dom G by FINSEQ_3:29;
set p = L (#) F;
A22: the carrier of W c= the carrier of V by VECTSP_4:def 2;
rng q c= the carrier of V by A22;
then reconsider q9 = q as FinSequence of V by FINSEQ_1:def 4;
consider f being Function of NAT, the carrier of W such that
A23: Sum q = f . (len q) and
A24: f . 0 = 0. W and
A25: for i being Nat
for w being Vector of W st i < len q & w = q . (i + 1) holds
f . (i + 1) = (f . i) + w by RLVECT_1:def 12;
( dom f = NAT & rng f c= the carrier of W ) by FUNCT_2:def 1;
then reconsider f9 = f as Function of NAT, the carrier of V by A22, FUNCT_2:2, XBOOLE_1:1;
A26: for i being Nat
for v being Vector of V st i < len q9 & v = q9 . (i + 1) holds
f9 . (i + 1) = (f9 . i) + v

let i be Nat; :: thesis:
let v be Vector of V; :: thesis:
assume that
A27: i < len q9 and
A28: v = q9 . (i + 1) ; :: thesis:
( 1 <= i + 1 & i + 1 <= len q ) by A27, NAT_1:11, NAT_1:13;
then i + 1 in dom q by FINSEQ_3:25;
then reconsider v9 = v as Vector of W by A28, FINSEQ_2:11;
f . (i + 1) = (f . i) + v9 by A25, A27, A28;
hence f9 . (i + 1) = (f9 . i) + v by ZMODUL01:28; :: thesis:

end;

let i be Nat; :: thesis:
set v = F /. i;
set j = P . i;
assume A34: i in dom (L (#) F) ; :: thesis:
then A35: F /. i = F . i by A30, A32, PARTFUN1:def 6;
then F /. i in rng F by A30, A32, A34, FUNCT_1:def 3;
then reconsider w = F /. i as Vector of W by A17, A11;
( dom P = dom G & rng P = dom G ) by FUNCT_2:52, FUNCT_2:def 3;
then A36: P . i in dom G by A32, A34, FUNCT_1:def 3;
then reconsider j = P . i as Element of NAT ;
A37: G /. j = G . (P . i) by A36, PARTFUN1:def 6
.= F /. i by A18, A30, A32, A34, A35, FUNCT_1:12 ;
q . i = (K (#) G) . j by A21, A32, A34, FUNCT_1:12
.= (K . w) * w by A33, A21, A36, A37, VECTSP_6:def 5
.= (L . (F /. i)) * w by A2, A3, FUNCT_1:47
.= (L . (F /. i)) * (F /. i) by ZMODUL01:29 ;
hence (L (#) F) . i = q . i by A34, VECTSP_6:def 5; :: thesis:

end;