let v1, v2 be Element 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 the carrier 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 the carrier 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_{1}[ object , object ] means {$2} = F1 " {(F2 . $1)};

A9: dom F2 = Seg (len F2) by FINSEQ_1:def 3;

A10: dom F1 = Seg (len F1) by FINSEQ_1:def 3;

A11: len F1 = len F2 by A3, A4, A6, A7, FINSEQ_1:48;

A12: for x being object st x in dom F1 holds

ex y being object st

( y in dom F1 & S_{1}[x,y] )

A14: for x being object st x in dom F1 holds

S_{1}[x,f . x]
from FUNCT_2:sch 1(A12);

A15: f is one-to-one

A21: len (L (#) F1) = len F1 by Def7;

A22: rng f = dom F1

( 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 A21;

set G2 = L (#) F2;

A27: dom (L (#) F2) = Seg (len (L (#) F2)) by FINSEQ_1:def 3;

A28: len (L (#) F2) = len F2 by Def7;

A29: dom (L (#) F1) = Seg (len (L (#) F1)) by FINSEQ_1:def 3;

( 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 the carrier 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 the carrier 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

A9: dom F2 = Seg (len F2) by FINSEQ_1:def 3;

A10: dom F1 = Seg (len F1) by FINSEQ_1:def 3;

A11: len F1 = len F2 by A3, A4, A6, A7, FINSEQ_1:48;

A12: for x being object st x in dom F1 holds

ex y being object st

( y in dom F1 & S

proof

consider f being Function of (dom F1),(dom F1) such that
let x be object ; :: thesis: ( x in dom F1 implies ex y being object st

( y in dom F1 & S_{1}[x,y] ) )

assume x in dom F1 ; :: thesis: ex y being object st

( y in dom F1 & S_{1}[x,y] )

then F2 . x in rng F1 by A4, A7, A11, A10, A9, 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_{1}[x,y] )

y in F1 " {(F2 . x)} by A13, TARSKI:def 1;

hence y in dom F1 by FUNCT_1:def 7; :: thesis: S_{1}[x,y]

thus S_{1}[x,y]
by A13; :: thesis: verum

end;( y in dom F1 & S

assume x in dom F1 ; :: thesis: ex y being object st

( y in dom F1 & S

then F2 . x in rng F1 by A4, A7, A11, A10, A9, 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

y in F1 " {(F2 . x)} by A13, TARSKI:def 1;

hence y in dom F1 by FUNCT_1:def 7; :: thesis: S

thus S

A14: for x being object st x in dom F1 holds

S

A15: f is one-to-one

proof

set G1 = L (#) F1;
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

A16: y1 in dom f and

A17: y2 in dom f and

A18: f . y1 = f . y2 ; :: thesis: y1 = y2

F2 . y1 in rng F1 by A4, A7, A11, A10, A9, A16, FUNCT_1:def 3;

then A19: {(F2 . y1)} c= rng F1 by ZFMISC_1:31;

F2 . y2 in rng F1 by A4, A7, A11, A10, A9, A17, FUNCT_1:def 3;

then A20: {(F2 . y2)} c= rng F1 by ZFMISC_1:31;

( F1 " {(F2 . y1)} = {(f . y1)} & F1 " {(F2 . y2)} = {(f . y2)} ) by A14, A16, A17;

then {(F2 . y1)} = {(F2 . y2)} by A18, A19, A20, FUNCT_1:91;

then F2 . y1 = F2 . y2 by ZFMISC_1:3;

hence y1 = y2 by A6, A11, A10, A9, A16, A17; :: thesis: verum

end;assume that

A16: y1 in dom f and

A17: y2 in dom f and

A18: f . y1 = f . y2 ; :: thesis: y1 = y2

F2 . y1 in rng F1 by A4, A7, A11, A10, A9, A16, FUNCT_1:def 3;

then A19: {(F2 . y1)} c= rng F1 by ZFMISC_1:31;

F2 . y2 in rng F1 by A4, A7, A11, A10, A9, A17, FUNCT_1:def 3;

then A20: {(F2 . y2)} c= rng F1 by ZFMISC_1:31;

( F1 " {(F2 . y1)} = {(f . y1)} & F1 " {(F2 . y2)} = {(f . y2)} ) by A14, A16, A17;

then {(F2 . y1)} = {(F2 . y2)} by A18, A19, A20, FUNCT_1:91;

then F2 . y1 = F2 . y2 by ZFMISC_1:3;

hence y1 = y2 by A6, A11, A10, A9, A16, A17; :: thesis: verum

A21: len (L (#) F1) = len F1 by Def7;

A22: rng f = dom F1

proof

then reconsider f = f as Permutation of (dom F1) by A15, FUNCT_2:57;
thus
rng f c= dom F1
; :: 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 A23: 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

A24: x in dom F2 and

A25: F2 . x = F1 . y by FUNCT_1:def 3;

F1 " {(F2 . x)} = F1 " (Im (F1,y)) by A23, A25, FUNCT_1:59;

then F1 " {(F2 . x)} c= {y} by A3, FUNCT_1:82;

then {(f . x)} c= {y} by A11, A10, A9, A14, A24;

then A26: f . x = y by ZFMISC_1:18;

x in dom f by A11, A10, A9, A24, FUNCT_2:def 1;

hence y in rng f by A26, FUNCT_1:def 3; :: thesis: verum

end;let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in dom F1 or y in rng f )

assume A23: 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

A24: x in dom F2 and

A25: F2 . x = F1 . y by FUNCT_1:def 3;

F1 " {(F2 . x)} = F1 " (Im (F1,y)) by A23, A25, FUNCT_1:59;

then F1 " {(F2 . x)} c= {y} by A3, FUNCT_1:82;

then {(f . x)} c= {y} by A11, A10, A9, A14, A24;

then A26: f . x = y by ZFMISC_1:18;

x in dom f by A11, A10, A9, A24, FUNCT_2:def 1;

hence y in rng f by A26, FUNCT_1:def 3; :: thesis: verum

( 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 A21;

set G2 = L (#) F2;

A27: dom (L (#) F2) = Seg (len (L (#) F2)) by FINSEQ_1:def 3;

A28: len (L (#) F2) = len F2 by Def7;

A29: 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)

hence
v1 = v2
by A3, A4, A5, A6, A7, A8, A21, A28, Th6, FINSEQ_1:48; :: thesis: verum(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 A30: i in dom (L (#) F2) ; :: thesis: (L (#) F2) . i = (L (#) F1) . (f . i)

then reconsider u = F2 . i as VECTOR of V by A28, A9, A27, FUNCT_1:102;

A31: ( (L (#) F2) . i = (L . (F2 /. i)) * (F2 /. i) & F2 . i = F2 /. i ) by A28, A9, A27, A30, Def7, PARTFUN1:def 6;

i in dom f by A11, A21, A28, A29, A27, A30, FUNCT_2:def 1;

then A32: f . i in dom F1 by A22, FUNCT_1:def 3;

then reconsider m = f . i as Element of NAT ;

reconsider v = F1 . m as VECTOR of V by A32, FUNCT_1:102;

{(F1 . (f . i))} = Im (F1,(f . i)) by A32, FUNCT_1:59

.= F1 .: (F1 " {(F2 . i)}) by A11, A28, A10, A27, A14, A30 ;

then A33: u = v by FUNCT_1:75, ZFMISC_1:18;

F1 . m = F1 /. m by A32, PARTFUN1:def 6;

hence (L (#) F2) . i = (L (#) F1) . (f . i) by A21, A10, A29, A32, A33, A31, Def7; :: thesis: verum

end;assume A30: i in dom (L (#) F2) ; :: thesis: (L (#) F2) . i = (L (#) F1) . (f . i)

then reconsider u = F2 . i as VECTOR of V by A28, A9, A27, FUNCT_1:102;

A31: ( (L (#) F2) . i = (L . (F2 /. i)) * (F2 /. i) & F2 . i = F2 /. i ) by A28, A9, A27, A30, Def7, PARTFUN1:def 6;

i in dom f by A11, A21, A28, A29, A27, A30, FUNCT_2:def 1;

then A32: f . i in dom F1 by A22, FUNCT_1:def 3;

then reconsider m = f . i as Element of NAT ;

reconsider v = F1 . m as VECTOR of V by A32, FUNCT_1:102;

{(F1 . (f . i))} = Im (F1,(f . i)) by A32, FUNCT_1:59

.= F1 .: (F1 " {(F2 . i)}) by A11, A28, A10, A27, A14, A30 ;

then A33: u = v by FUNCT_1:75, ZFMISC_1:18;

F1 . m = F1 /. m by A32, PARTFUN1:def 6;

hence (L (#) F2) . i = (L (#) F1) . (f . i) by A21, A10, A29, A32, A33, A31, Def7; :: thesis: verum