let L be Z_Lattice; :: thesis: for F, F0 being FinSequence of L
for l being Linear_Combination of L
for v being Vector of L st F is one-to-one & F0 is one-to-one & Carrier l c= rng F & canFS (Carrier l) = F0 holds
Sum (ScFS (v,l,F)) = Sum (ScFS (v,l,F0))
let F, F0 be FinSequence of L; :: thesis: for l being Linear_Combination of L
for v being Vector of L st F is one-to-one & F0 is one-to-one & Carrier l c= rng F & canFS (Carrier l) = F0 holds
Sum (ScFS (v,l,F)) = Sum (ScFS (v,l,F0))
let l be Linear_Combination of L; :: thesis: for v being Vector of L st F is one-to-one & F0 is one-to-one & Carrier l c= rng F & canFS (Carrier l) = F0 holds
Sum (ScFS (v,l,F)) = Sum (ScFS (v,l,F0))
let v be Vector of L; :: thesis: ( F is one-to-one & F0 is one-to-one & Carrier l c= rng F & canFS (Carrier l) = F0 implies Sum (ScFS (v,l,F)) = Sum (ScFS (v,l,F0)) )
assume that
A1: F is one-to-one and
A2: F0 is one-to-one and
A3: Carrier l c= rng F and
A4: canFS (Carrier l) = F0 ; :: thesis: Sum (ScFS (v,l,F)) = Sum (ScFS (v,l,F0))
A51: card (dom F) = card (rng F) by A1, CARD_1:5, WELLORD2:def 4;
then A5: len F = card (rng F) by CARD_1:62;
Q1: ( F0 is one-to-one & rng F0 = Carrier l ) by A4, FUNCT_2:def 3;
FA5: card (dom F0) = card (rng F0) by A2, CARD_1:5, WELLORD2:def 4;
R1: len F0 = card (Carrier l) by A4, FINSEQ_1:93;
set CLN = (rng F) \ (Carrier l);
reconsider CLN = (rng F) \ (Carrier l) as finite Subset of L ;
set g = canFS CLN;
Q2: ( canFS CLN is one-to-one & rng (canFS CLN) = CLN ) by FUNCT_2:def 3;
R2: len (canFS CLN) = card CLN by FINSEQ_1:93;
reconsider g = canFS CLN as FinSequence of L by Q2, FINSEQ_1:def 4;
set H = F0 ^ g;
reconsider H = F0 ^ g as FinSequence of L ;
(rng F0) /\ (rng g) = (Carrier l) /\ CLN by Q1, FUNCT_2:def 3
.= ((Carrier l) /\ (rng F)) \ (Carrier l) by XBOOLE_1:49
.= (Carrier l) \ (Carrier l) by A3, XBOOLE_1:28
.= {} by XBOOLE_1:37 ;
then rng F0 misses rng g ;
then Q31: H is one-to-one by A4, FINSEQ_3:91;
Q32: rng H = (rng F0) \/ (rng g) by FINSEQ_1:31
.= (Carrier l) \/ ((rng F) \ (Carrier l)) by Q1, FUNCT_2:def 3
.= rng F by A3, XBOOLE_1:45 ;
C12: (card CLN) + (card (Carrier l)) = ((card (rng F)) - (card (Carrier l))) + (card (Carrier l)) by A3, CARD_2:44
.= card (rng F) ;
R3: len H = (len F0) + (len g) by FINSEQ_1:22
.= card (rng F) by C12, R1, FINSEQ_1:93 ;
then R4: dom H = Seg (card (rng F)) by FINSEQ_1:def 3;
set P = (F ") * H;
T3: dom (F ") = rng H by A1, Q32, FUNCT_1:33;
then T4: dom ((F ") * H) = dom H by RELAT_1:27
.= Seg (card (rng F)) by R3, FINSEQ_1:def 3 ;
T5: rng ((F ") * H) = rng (F ") by RELAT_1:28, T3
.= dom F by FUNCT_1:33, A1
.= Seg (card (rng F)) by A5, FINSEQ_1:def 3 ;
then reconsider P = (F ") * H as Function of (Seg (card (rng F))),(Seg (card (rng F))) by T4, FUNCT_2:1;
P is onto by T5;
then reconsider P = P as Permutation of (Seg (card (rng F))) by A1, Q31;
R5: len (ScFS (v,l,F)) = len F by defScFS
.= card (rng F) by A51, CARD_1:62 ;
then R6: dom (ScFS (v,l,F)) = Seg (card (rng F)) by FINSEQ_1:def 3;
len (ScFS (v,l,F0)) = len F0 by defScFS
.= card (rng F0) by FA5, CARD_1:62 ;
then XR6: dom (ScFS (v,l,F0)) = Seg (card (rng F0)) by FINSEQ_1:def 3;
R7: len (ScFS (v,l,H)) = card (rng F) by R3, defScFS;
then R8: dom (ScFS (v,l,H)) = Seg (card (rng F)) by FINSEQ_1:def 3;
R9: for i being Nat st i in dom (ScFS (v,l,F)) holds
(ScFS (v,l,H)) . i = (ScFS (v,l,F)) . (P . i)

proof

let i be Nat; :: thesis: ( i in dom (ScFS (v,l,F)) implies (ScFS (v,l,H)) . i = (ScFS (v,l,F)) . (P . i) )
assume R90: i in dom (ScFS (v,l,F)) ; :: thesis: (ScFS (v,l,H)) . i = (ScFS (v,l,F)) . (P . i)
then i in dom (ScFS (v,l,H)) by R6, R7, FINSEQ_1:def 3;
then R92: (ScFS (v,l,H)) . i = <;v,((l . (H /. i)) * (H /. i));> by defScFS;
S3: H . i in dom (F ") by R4, R6, R90, T3, FUNCT_1:3;
then (F ") . (H . i) in rng (F ") by FUNCT_1:3;
then S4: (F ") . (H . i) in dom F by FUNCT_1:33, A1;
S5: H . i in rng F by A1, FUNCT_1:33, S3;
F /. (P . i) = F /. ((F ") . (H . i)) by R6, R90, T4, FUNCT_1:12
.= F . ((F ") . (H . i)) by S4, PARTFUN1:def 6
.= H . i by FUNCT_1:35, A1, S5
.= H /. i by R4, R6, R90, PARTFUN1:def 6 ;
hence (ScFS (v,l,H)) . i = (ScFS (v,l,F)) . (P . i) by R6, R90, R92, defScFS, FUNCT_2:5; :: thesis: verum

end;

set K = (Seg (card CLN)) --> (0. F_Real);
rng ((Seg (card CLN)) --> (0. F_Real)) c= the carrier of F_Real ;
then reconsider K = (Seg (card CLN)) --> (0. F_Real) as FinSequence of F_Real by FINSEQ_1:def 4;
K100: dom K = Seg (card CLN) by FUNCT_2:def 1;
K2: dom ((ScFS (v,l,F0)) ^ K) = Seg ((len (ScFS (v,l,F0))) + (len K)) by FINSEQ_1:def 7
.= Seg ((len F0) + (len K)) by defScFS
.= Seg ((card (Carrier l)) + (card CLN)) by R1, K100, FINSEQ_1:def 3
.= dom (ScFS (v,l,H)) by C12, R7, FINSEQ_1:def 3 ;
for k being Nat st k in dom (ScFS (v,l,H)) holds
(ScFS (v,l,H)) . k = ((ScFS (v,l,F0)) ^ K) . k

proof

let k be Nat; :: thesis: ( k in dom (ScFS (v,l,H)) implies (ScFS (v,l,H)) . k = ((ScFS (v,l,F0)) ^ K) . k )
assume K3: k in dom (ScFS (v,l,H)) ; :: thesis: (ScFS (v,l,H)) . k = ((ScFS (v,l,F0)) ^ K) . k
then L4: ( 1 <= k & k <= card (rng F) ) by R8, FINSEQ_1:1;
L5: card (rng F) = (len F0) + (len g) by C12, R1, FINSEQ_1:93;
K4: (ScFS (v,l,H)) . k = <;v,((l . (H /. k)) * (H /. k));> by defScFS, K3;

per cases ( k <= len F0 or len F0 < k ) ;

suppose CAS2: k <= len F0 ; :: thesis: (ScFS (v,l,H)) . k = ((ScFS (v,l,F0)) ^ K) . k

then CAS21: k in dom F0 by FINSEQ_3:25, L4;
then H . k = F0 . k by FINSEQ_1:def 7;
then H . k = F0 /. k by CAS21, PARTFUN1:def 6;
then CAS3: H /. k = F0 /. k by K3, R4, R8, PARTFUN1:def 6;
CAS4: k in dom (ScFS (v,l,F0)) by CAS2, L4, XR6, R1, Q1;
then ((ScFS (v,l,F0)) ^ K) . k = (ScFS (v,l,F0)) . k by FINSEQ_1:def 7
.= <;v,((l . (F0 /. k)) * (F0 /. k));> by CAS4, defScFS ;
hence (ScFS (v,l,H)) . k = ((ScFS (v,l,F0)) ^ K) . k by K3, CAS3, defScFS; :: thesis: verum

end;

suppose len F0 < k ; :: thesis: (ScFS (v,l,H)) . k = ((ScFS (v,l,F0)) ^ K) . k

then CAS7: k - (len F0) > 0 by XREAL_1:50;
then k - (len F0) in NAT by INT_1:3;
then reconsider k1 = k - (len F0) as Nat ;
CAS8: 1 <= k1 by NAT_1:14, CAS7;
k1 <= ((len F0) + (len g)) - (len F0) by L4, L5, XREAL_1:9;
then CAS100: k1 in Seg (len g) by CAS8;
then CAS10: k1 in dom g by FINSEQ_1:def 3;
then H . ((len F0) + k1) = g . k1 by FINSEQ_1:def 7;
then H . k in CLN by CAS10, Q2, FUNCT_1:3;
then H /. k in CLN by K3, R4, R8, PARTFUN1:def 6;
then CAS11: not H /. k in Carrier l by XBOOLE_0:def 5;
X1: ((ScFS (v,l,F0)) ^ K) . ((len (ScFS (v,l,F0))) + k1) = K . k1 by CAS100, K100, R2, FINSEQ_1:def 7
.= 0. F_Real by R2, CAS100, FUNCOP_1:7 ;
CAS5: (len (ScFS (v,l,F0))) + k1 = (len F0) + k1 by defScFS;
(ScFS (v,l,H)) . k = <;v,((0. INT.Ring) * (H /. k));> by K4, CAS11
.= <;((0. INT.Ring) * (H /. k)),v;> by ZMODLAT1:def 3
.= (0. INT.Ring) * <;(H /. k),v;> by ZMODLAT1:def 3
.= 0. INT.Ring ;
hence (ScFS (v,l,H)) . k = ((ScFS (v,l,F0)) ^ K) . k by CAS5, X1; :: thesis: verum

end;

end;

end;

then R11: ScFS (v,l,H) = (ScFS (v,l,F0)) ^ K by K2;
Sum (ScFS (v,l,H)) = (Sum (ScFS (v,l,F0))) + (Sum K) by R11, RLVECT_1:41
.= (Sum (ScFS (v,l,F0))) + (0. F_Real) by LM0
.= Sum (ScFS (v,l,F0)) ;
hence Sum (ScFS (v,l,F)) = Sum (ScFS (v,l,F0)) by R6, R8, R9, R7, R5, RLVECT_2:6; :: thesis: verum