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 () = 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 () = 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 () = 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 () = 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 () = F0 ; :: thesis: Sum (ScFS (v,l,F)) = Sum (ScFS (v,l,F0))
A51: card (dom F) = card (rng F) by ;
then A5: len F = card (rng F) by CARD_1:62;
Q1: ( F0 is one-to-one & rng F0 = Carrier l ) by ;
FA5: card (dom F0) = card (rng F0) by ;
R1: len F0 = card () by ;
set CLN = (rng F) \ ();
reconsider CLN = (rng F) \ () 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 ;
set H = F0 ^ g;
reconsider H = F0 ^ g as FinSequence of L ;
(rng F0) /\ (rng g) = () /\ CLN by
.= (() /\ (rng F)) \ () by XBOOLE_1:49
.= () \ () by
.= {} by XBOOLE_1:37 ;
then rng F0 misses rng g ;
then Q31: H is one-to-one by ;
Q32: rng H = (rng F0) \/ (rng g) by FINSEQ_1:31
.= () \/ ((rng F) \ ()) by
.= rng F by ;
C12: (card CLN) + (card ()) = ((card (rng F)) - (card ())) + (card ()) by
.= card (rng F) ;
R3: len H = (len F0) + (len g) by FINSEQ_1:22
.= card (rng F) by ;
then R4: dom H = Seg (card (rng F)) by FINSEQ_1:def 3;
set P = (F ") * H;
T3: dom (F ") = rng H by ;
then T4: dom ((F ") * H) = dom H by RELAT_1:27
.= Seg (card (rng F)) by ;
T5: rng ((F ") * H) = rng (F ") by
.= dom F by
.= Seg (card (rng F)) by ;
then reconsider P = (F ") * H as Function of (Seg (card (rng F))),(Seg (card (rng F))) by ;
P is onto by T5;
then reconsider P = P as Permutation of (Seg (card (rng F))) by ;
R5: len (ScFS (v,l,F)) = len F by defScFS
.= card (rng F) by ;
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 ;
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 ;
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 ;
then R92: (ScFS (v,l,H)) . i = <;v,((l . (H /. i)) * (H /. i));> by defScFS;
S3: H . i in dom (F ") by ;
then (F ") . (H . i) in rng (F ") by FUNCT_1:3;
then S4: (F ") . (H . i) in dom F by ;
S5: H . i in rng F by ;
F /. (P . i) = F /. ((F ") . (H . i)) by
.= F . ((F ") . (H . i)) by
.= H . i by
.= H /. i by ;
hence (ScFS (v,l,H)) . i = (ScFS (v,l,F)) . (P . i) by ; :: thesis: verum
end;
set K = (Seg (card CLN)) --> ();
rng ((Seg (card CLN)) --> ()) c= the carrier of F_Real ;
then reconsider K = (Seg (card CLN)) --> () 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 ()) + (card CLN)) by
.= dom (ScFS (v,l,H)) by ;
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 ;
L5: card (rng F) = (len F0) + (len g) by ;
K4: (ScFS (v,l,H)) . k = <;v,((l . (H /. k)) * (H /. k));> by ;
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 ;
then H . k = F0 . k by FINSEQ_1:def 7;
then H . k = F0 /. k by ;
then CAS3: H /. k = F0 /. k by ;
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 ;
hence (ScFS (v,l,H)) . k = ((ScFS (v,l,F0)) ^ K) . k by ; :: 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 ;
k1 <= ((len F0) + (len g)) - (len F0) by ;
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 ;
then H /. k in CLN by ;
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
.= 0. F_Real by ;
CAS5: (len (ScFS (v,l,F0))) + k1 = (len F0) + k1 by defScFS;
(ScFS (v,l,H)) . k = <;v,(() * (H /. k));> by
.= <;(() * (H /. k)),v;> by ZMODLAT1:def 3
.= () * <;(H /. k),v;> by ZMODLAT1:def 3
.= 0. INT.Ring ;
hence (ScFS (v,l,H)) . k = ((ScFS (v,l,F0)) ^ K) . k by ; :: 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
.= (Sum (ScFS (v,l,F0))) + () 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