let v1, v2 be Vector of V; :: thesis: ( ex F being FinSequence of V st
( F is one-to-one & rng F = Carrier L & v1 = Sum (L (#) F) ) & ex F being FinSequence of V st
( F is one-to-one & rng F = Carrier L & v2 = Sum (L (#) F) ) implies v1 = v2 )
given F1 being FinSequence of V such that A3: F1 is one-to-one and
A4: rng F1 = Carrier L and
A5: v1 = Sum (L (#) F1) ; :: thesis: ( for F being FinSequence of V holds
( not F is one-to-one or not rng F = Carrier L or not v2 = Sum (L (#) F) ) or v1 = v2 )
given F2 being FinSequence of V such that A6: F2 is one-to-one and
A7: rng F2 = Carrier L and
A8: v2 = Sum (L (#) F2) ; :: thesis: v1 = v2
defpred S₁[ object , object ] means {$2} = F1 " {(F2 . $1)};
A9: len F1 = len F2 by A3, A4, A6, A7, FINSEQ_1:48;
A10: dom F1 = Seg (len F1) by FINSEQ_1:def 3;
A11: dom F2 = Seg (len F2) by FINSEQ_1:def 3;
A12: for x being object st x in dom F1 holds
ex y being object st
( y in dom F1 & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in dom F1 implies ex y being object st
( y in dom F1 & S₁[x,y] ) )
assume x in dom F1 ; :: thesis: ex y being object st
( y in dom F1 & S₁[x,y] )
then F2 . x in rng F1 by A4, A7, A9, A10, A11, FUNCT_1:def 3;
then consider y being object such that
A13: F1 " {(F2 . x)} = {y} by A3, FUNCT_1:74;
take y ; :: thesis: ( y in dom F1 & S₁[x,y] )
y in F1 " {(F2 . x)} by A13, TARSKI:def 1;
hence y in dom F1 by FUNCT_1:def 7; :: thesis: S₁[x,y]
thus S₁[x,y] by A13; :: thesis: verum

end;

consider f being Function of (dom F1),(dom F1) such that
A14: for x being object st x in dom F1 holds
S₁[x,f . x] from FUNCT_2:sch 1(A12);
A15: rng f = dom F1

proof

thus rng f c= dom F1 by RELAT_1:def 19; :: according to XBOOLE_0:def 10 :: thesis: dom F1 c= rng f
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in dom F1 or y in rng f )
assume A16: y in dom F1 ; :: thesis: y in rng f
then F1 . y in rng F2 by A4, A7, FUNCT_1:def 3;
then consider x being object such that
A17: x in dom F2 and
A18: F2 . x = F1 . y by FUNCT_1:def 3;
F1 " {(F2 . x)} = F1 " (Im (F1,y)) by A16, A18, FUNCT_1:59;
then F1 " {(F2 . x)} c= {y} by A3, FUNCT_1:82;
then {(f . x)} c= {y} by A9, A10, A11, A14, A17;
then A19: f . x = y by ZFMISC_1:18;
x in dom f by A9, A10, A11, A17, FUNCT_2:def 1;
hence y in rng f by A19, FUNCT_1:def 3; :: thesis: verum

end;

set G1 = L (#) F1;
A20: len (L (#) F1) = len F1 by Def6;
A21: ( dom F1 = {} implies dom F1 = {} ) ;
A22: f is one-to-one

proof

let y1, y2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not y1 in dom f or not y2 in dom f or not f . y1 = f . y2 or y1 = y2 )
assume that
A23: y1 in dom f and
A24: y2 in dom f and
A25: f . y1 = f . y2 ; :: thesis: y1 = y2
A26: y2 in dom F1 by A21, A24, FUNCT_2:def 1;
then A27: F1 " {(F2 . y2)} = {(f . y2)} by A14;
A28: y1 in dom F1 by A21, A23, FUNCT_2:def 1;
then F2 . y1 in rng F1 by A4, A7, A9, A10, A11, FUNCT_1:def 3;
then A29: {(F2 . y1)} c= rng F1 by ZFMISC_1:31;
F2 . y2 in rng F1 by A4, A7, A9, A10, A11, A26, FUNCT_1:def 3;
then A30: {(F2 . y2)} c= rng F1 by ZFMISC_1:31;
F1 " {(F2 . y1)} = {(f . y1)} by A14, A28;
then {(F2 . y1)} = {(F2 . y2)} by A25, A27, A29, A30, FUNCT_1:91;
then A31: F2 . y1 = F2 . y2 by ZFMISC_1:3;
( y1 in dom F2 & y2 in dom F2 ) by A9, A10, A11, A21, A23, A24, FUNCT_2:def 1;
hence y1 = y2 by A6, A31; :: thesis: verum

end;

set G2 = L (#) F2;
A32: dom (L (#) F2) = Seg (len (L (#) F2)) by FINSEQ_1:def 3;
reconsider f = f as Permutation of (dom F1) by A15, A22, FUNCT_2:57;
( dom F1 = Seg (len F1) & dom (L (#) F1) = Seg (len (L (#) F1)) ) by FINSEQ_1:def 3;
then reconsider f = f as Permutation of (dom (L (#) F1)) by A20;
A33: len (L (#) F2) = len F2 by Def6;
A34: dom (L (#) F1) = Seg (len (L (#) F1)) by FINSEQ_1:def 3;

now :: thesis: for i being Nat st i in dom (L (#) F2) holds
(L (#) F2) . i = (L (#) F1) . (f . i)

let i be Nat; :: thesis: ( i in dom (L (#) F2) implies (L (#) F2) . i = (L (#) F1) . (f . i) )
assume A35: i in dom (L (#) F2) ; :: thesis: (L (#) F2) . i = (L (#) F1) . (f . i)
then A36: ( (L (#) F2) . i = (F2 /. i) * (L . (F2 /. i)) & F2 . i = F2 /. i ) by A33, A11, A32, Def6, PARTFUN1:def 6;
i in dom F2 by A33, A35, FINSEQ_3:29;
then reconsider u = F2 . i as Vector of V by FINSEQ_2:11;
i in dom f by A9, A20, A33, A34, A32, A35, FUNCT_2:def 1;
then A37: f . i in dom F1 by A15, FUNCT_1:def 3;
then reconsider m = f . i as Element of NAT by A10;
reconsider v = F1 . m as Vector of V by A37, FINSEQ_2:11;
{(F1 . (f . i))} = Im (F1,(f . i)) by A37, FUNCT_1:59
.= F1 .: (F1 " {(F2 . i)}) by A9, A33, A10, A32, A14, A35 ;
then A38: u = v by FUNCT_1:75, ZFMISC_1:18;
F1 . m = F1 /. m by A37, PARTFUN1:def 6;
hence (L (#) F2) . i = (L (#) F1) . (f . i) by A20, A10, A34, A37, A38, A36, Def6; :: thesis: verum

end;

hence v1 = v2 by A3, A4, A5, A6, A7, A8, A20, A33, FINSEQ_1:48, RLVECT_2:6; :: thesis: verum