let L be Z_Lattice; 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; 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; 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; ( 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
; 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;
( 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))
;
(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;
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;
( 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))
;
(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
;
(ScFS (v,l,H)) . k = ((ScFS (v,l,F0)) ^ K) . kthen 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;
verum end; suppose
len F0 < k
;
(ScFS (v,l,H)) . k = ((ScFS (v,l,F0)) ^ K) . kthen 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;
verum 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; verum