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