let S1, S2 be Real; :: thesis: ( ex F being FinSequence of S st

( F is one-to-one & rng F = Carrier LS & S1 = Sum (LS * F) ) & ex F being FinSequence of S st

( F is one-to-one & rng F = Carrier LS & S2 = Sum (LS * F) ) implies S1 = S2 )

given F1 being FinSequence of S such that A3: F1 is one-to-one and

A4: rng F1 = Carrier LS and

A5: S1 = Sum (LS * F1) ; :: thesis: ( for F being FinSequence of S holds

( not F is one-to-one or not rng F = Carrier LS or not S2 = Sum (LS * F) ) or S1 = S2 )

A6: dom (F1 ") = Carrier LS by A3, A4, FUNCT_1:33;

A7: len F1 = card (Carrier LS) by A3, A4, FINSEQ_4:62;

given F2 being FinSequence of S such that A8: F2 is one-to-one and

A9: rng F2 = Carrier LS and

A10: S2 = Sum (LS * F2) ; :: thesis: S1 = S2

set F12 = (F1 ") * F2;

( dom F2 = Seg (len F2) & len F2 = card (Carrier LS) ) by A8, A9, FINSEQ_1:def 3, FINSEQ_4:62;

then A11: dom ((F1 ") * F2) = Seg (len F1) by A6, A7, A9, RELAT_1:27;

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

then rng (F1 ") = Seg (len F1) by A3, FUNCT_1:33;

then A12: rng ((F1 ") * F2) = Seg (len F1) by A6, A9, RELAT_1:28;

then reconsider F12 = (F1 ") * F2 as Function of (Seg (len F1)),(Seg (len F1)) by A11, FUNCT_2:1;

A13: F12 is onto by A12, FUNCT_2:def 3;

len (LS * F1) = len F1 by FINSEQ_2:33;

then dom (LS * F1) = Seg (len F1) by FINSEQ_1:def 3;

then reconsider F12 = F12 as Permutation of (dom (LS * F1)) by A3, A8, A13;

(LS * F1) * F12 = LS * (F1 * F12) by RELAT_1:36

.= LS * ((F1 * (F1 ")) * F2) by RELAT_1:36

.= LS * ((id (Carrier LS)) * F2) by A3, A4, FUNCT_1:39

.= LS * F2 by A9, RELAT_1:53 ;

hence S1 = S2 by A5, A10, FINSOP_1:7; :: thesis: verum

( F is one-to-one & rng F = Carrier LS & S1 = Sum (LS * F) ) & ex F being FinSequence of S st

( F is one-to-one & rng F = Carrier LS & S2 = Sum (LS * F) ) implies S1 = S2 )

given F1 being FinSequence of S such that A3: F1 is one-to-one and

A4: rng F1 = Carrier LS and

A5: S1 = Sum (LS * F1) ; :: thesis: ( for F being FinSequence of S holds

( not F is one-to-one or not rng F = Carrier LS or not S2 = Sum (LS * F) ) or S1 = S2 )

A6: dom (F1 ") = Carrier LS by A3, A4, FUNCT_1:33;

A7: len F1 = card (Carrier LS) by A3, A4, FINSEQ_4:62;

given F2 being FinSequence of S such that A8: F2 is one-to-one and

A9: rng F2 = Carrier LS and

A10: S2 = Sum (LS * F2) ; :: thesis: S1 = S2

set F12 = (F1 ") * F2;

( dom F2 = Seg (len F2) & len F2 = card (Carrier LS) ) by A8, A9, FINSEQ_1:def 3, FINSEQ_4:62;

then A11: dom ((F1 ") * F2) = Seg (len F1) by A6, A7, A9, RELAT_1:27;

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

then rng (F1 ") = Seg (len F1) by A3, FUNCT_1:33;

then A12: rng ((F1 ") * F2) = Seg (len F1) by A6, A9, RELAT_1:28;

then reconsider F12 = (F1 ") * F2 as Function of (Seg (len F1)),(Seg (len F1)) by A11, FUNCT_2:1;

A13: F12 is onto by A12, FUNCT_2:def 3;

len (LS * F1) = len F1 by FINSEQ_2:33;

then dom (LS * F1) = Seg (len F1) by FINSEQ_1:def 3;

then reconsider F12 = F12 as Permutation of (dom (LS * F1)) by A3, A8, A13;

(LS * F1) * F12 = LS * (F1 * F12) by RELAT_1:36

.= LS * ((F1 * (F1 ")) * F2) by RELAT_1:36

.= LS * ((id (Carrier LS)) * F2) by A3, A4, FUNCT_1:39

.= LS * F2 by A9, RELAT_1:53 ;

hence S1 = S2 by A5, A10, FINSOP_1:7; :: thesis: verum