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)

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

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

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

set K = (Seg (card CLN)) --> (0. F_Real);
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;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

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

then R11:
ScFS (v,l,H) = (ScFS (v,l,F0)) ^ K
by K2;
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;

end;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 )
;

end;

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

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

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