let L be Z_Lattice; :: thesis: for v being Vector of ()
for l1, l2 being Linear_Combination of DivisibleMod L holds SumSc (v,(l1 + l2)) = (SumSc (v,l1)) + (SumSc (v,l2))

let w be Vector of (); :: thesis: for l1, l2 being Linear_Combination of DivisibleMod L holds SumSc (w,(l1 + l2)) = (SumSc (w,l1)) + (SumSc (w,l2))
let l1, l2 be Linear_Combination of DivisibleMod L; :: thesis: SumSc (w,(l1 + l2)) = (SumSc (w,l1)) + (SumSc (w,l2))
set A = ((Carrier (l1 + l2)) \/ (Carrier l1)) \/ (Carrier l2);
set C1 = (((Carrier (l1 + l2)) \/ (Carrier l1)) \/ (Carrier l2)) \ (Carrier l1);
consider p being FinSequence such that
A1: rng p = (((Carrier (l1 + l2)) \/ (Carrier l1)) \/ (Carrier l2)) \ (Carrier l1) and
A2: p is one-to-one by FINSEQ_4:58;
reconsider p = p as FinSequence of () by ;
A3: ((Carrier (l1 + l2)) \/ (Carrier l1)) \/ (Carrier l2) = (Carrier l1) \/ ((Carrier (l1 + l2)) \/ (Carrier l2)) by XBOOLE_1:4;
set C3 = (((Carrier (l1 + l2)) \/ (Carrier l1)) \/ (Carrier l2)) \ (Carrier (l1 + l2));
consider r being FinSequence such that
A4: rng r = (((Carrier (l1 + l2)) \/ (Carrier l1)) \/ (Carrier l2)) \ (Carrier (l1 + l2)) and
A5: r is one-to-one by FINSEQ_4:58;
reconsider r = r as FinSequence of () by ;
A6: ((Carrier (l1 + l2)) \/ (Carrier l1)) \/ (Carrier l2) = (Carrier (l1 + l2)) \/ ((Carrier l1) \/ (Carrier l2)) by XBOOLE_1:4;
set C2 = (((Carrier (l1 + l2)) \/ (Carrier l1)) \/ (Carrier l2)) \ (Carrier l2);
consider q being FinSequence such that
A7: rng q = (((Carrier (l1 + l2)) \/ (Carrier l1)) \/ (Carrier l2)) \ (Carrier l2) and
A8: q is one-to-one by FINSEQ_4:58;
reconsider q = q as FinSequence of () by ;
consider F being FinSequence of () such that
A9: F is one-to-one and
A10: rng F = Carrier (l1 + l2) and
A11: SumSc (w,(l1 + l2)) = Sum (ScFS (w,(l1 + l2),F)) by defSumScDM;
set FF = F ^ r;
consider G being FinSequence of () such that
A12: G is one-to-one and
A13: rng G = Carrier l1 and
A14: SumSc (w,l1) = Sum (ScFS (w,l1,G)) by defSumScDM;
rng (F ^ r) = (rng F) \/ (rng r) by FINSEQ_1:31;
then rng (F ^ r) = (Carrier (l1 + l2)) \/ (((Carrier (l1 + l2)) \/ (Carrier l1)) \/ (Carrier l2)) by ;
then A15: rng (F ^ r) = ((Carrier (l1 + l2)) \/ (Carrier l1)) \/ (Carrier l2) by ;
set GG = G ^ p;
rng (G ^ p) = (rng G) \/ (rng p) by FINSEQ_1:31;
then rng (G ^ p) = (Carrier l1) \/ (((Carrier (l1 + l2)) \/ (Carrier l1)) \/ (Carrier l2)) by ;
then A16: rng (G ^ p) = ((Carrier (l1 + l2)) \/ (Carrier l1)) \/ (Carrier l2) by ;
rng F misses rng r
proof
set x = the Element of (rng F) /\ (rng r);
assume not rng F misses rng r ; :: thesis: contradiction
then ( the Element of (rng F) /\ (rng r) in Carrier (l1 + l2) & the Element of (rng F) /\ (rng r) in (((Carrier (l1 + l2)) \/ (Carrier l1)) \/ (Carrier l2)) \ (Carrier (l1 + l2)) ) by ;
hence contradiction by XBOOLE_0:def 5; :: thesis: verum
end;
then A17: F ^ r is one-to-one by ;
rng G misses rng p
proof
set x = the Element of (rng G) /\ (rng p);
assume not rng G misses rng p ; :: thesis: contradiction
then ( the Element of (rng G) /\ (rng p) in Carrier l1 & the Element of (rng G) /\ (rng p) in (((Carrier (l1 + l2)) \/ (Carrier l1)) \/ (Carrier l2)) \ (Carrier l1) ) by ;
hence contradiction by XBOOLE_0:def 5; :: thesis: verum
end;
then A18: G ^ p is one-to-one by ;
then A19: len (G ^ p) = len (F ^ r) by ;
deffunc H1( Nat) -> set = (F ^ r) <- ((G ^ p) . \$1);
consider P being FinSequence such that
A20: len P = len (F ^ r) and
A21: for k being Nat st k in dom P holds
P . k = H1(k) from A22: dom P = Seg (len (F ^ r)) by ;
A23: now :: thesis: for x being object st x in dom (G ^ p) holds
(G ^ p) . x = (F ^ r) . (P . x)
let x be object ; :: thesis: ( x in dom (G ^ p) implies (G ^ p) . x = (F ^ r) . (P . x) )
assume A24: x in dom (G ^ p) ; :: thesis: (G ^ p) . x = (F ^ r) . (P . x)
then reconsider n = x as Element of NAT ;
(G ^ p) . n in rng (F ^ r) by ;
then A25: F ^ r just_once_values (G ^ p) . n by ;
n in Seg (len (F ^ r)) by ;
then (F ^ r) . (P . n) = (F ^ r) . ((F ^ r) <- ((G ^ p) . n)) by
.= (G ^ p) . n by ;
hence (G ^ p) . x = (F ^ r) . (P . x) ; :: thesis: verum
end;
A26: rng P c= dom (F ^ r)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng P or x in dom (F ^ r) )
assume x in rng P ; :: thesis: x in dom (F ^ r)
then consider y being object such that
A27: y in dom P and
A28: P . y = x by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A27;
y in dom (G ^ p) by ;
then (G ^ p) . y in rng (F ^ r) by ;
then A29: F ^ r just_once_values (G ^ p) . y by ;
P . y = (F ^ r) <- ((G ^ p) . y) by ;
hence x in dom (F ^ r) by ; :: thesis: verum
end;
now :: thesis: for x being object holds
( ( x in dom (G ^ p) implies ( x in dom P & P . x in dom (F ^ r) ) ) & ( x in dom P & P . x in dom (F ^ r) implies x in dom (G ^ p) ) )
let x be object ; :: thesis: ( ( x in dom (G ^ p) implies ( x in dom P & P . x in dom (F ^ r) ) ) & ( x in dom P & P . x in dom (F ^ r) implies x in dom (G ^ p) ) )
thus ( x in dom (G ^ p) implies ( x in dom P & P . x in dom (F ^ r) ) ) :: thesis: ( x in dom P & P . x in dom (F ^ r) implies x in dom (G ^ p) )
proof
assume x in dom (G ^ p) ; :: thesis: ( x in dom P & P . x in dom (F ^ r) )
then x in Seg (len P) by ;
hence x in dom P by FINSEQ_1:def 3; :: thesis: P . x in dom (F ^ r)
then P . x in rng P by FUNCT_1:def 3;
hence P . x in dom (F ^ r) by A26; :: thesis: verum
end;
assume that
A30: x in dom P and
P . x in dom (F ^ r) ; :: thesis: x in dom (G ^ p)
x in Seg (len P) by ;
hence x in dom (G ^ p) by ; :: thesis: verum
end;
then A31: G ^ p = (F ^ r) * P by ;
dom (F ^ r) c= rng P
proof
set f = ((F ^ r) ") * (G ^ p);
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (F ^ r) or x in rng P )
assume A32: x in dom (F ^ r) ; :: thesis: x in rng P
dom ((F ^ r) ") = rng (G ^ p) by ;
then A33: rng (((F ^ r) ") * (G ^ p)) = rng ((F ^ r) ") by RELAT_1:28
.= dom (F ^ r) by ;
((F ^ r) ") * (G ^ p) = (((F ^ r) ") * (F ^ r)) * P by
.= (id (dom (F ^ r))) * P by
.= P by ;
hence x in rng P by ; :: thesis: verum
end;
then A34: dom (F ^ r) = rng P by A26;
A35: len r = len (ScFS (w,(l1 + l2),r)) by defScFSDM;
B1: dom r = Seg (len r) by FINSEQ_1:def 3
.= Seg (len (ScFS (w,(l1 + l2),r))) by defScFSDM
.= dom (ScFS (w,(l1 + l2),r)) by FINSEQ_1:def 3 ;
now :: thesis: for k being Nat st k in dom (ScFS (w,(l1 + l2),r)) holds
(ScFS (w,(l1 + l2),r)) . k = - ((ScFS (w,(l1 + l2),r)) /. k)
let k be Nat; :: thesis: ( k in dom (ScFS (w,(l1 + l2),r)) implies (ScFS (w,(l1 + l2),r)) . k = - ((ScFS (w,(l1 + l2),r)) /. k) )
assume A36: k in dom (ScFS (w,(l1 + l2),r)) ; :: thesis: (ScFS (w,(l1 + l2),r)) . k = - ((ScFS (w,(l1 + l2),r)) /. k)
then r /. k = r . k by ;
then r /. k in (((Carrier (l1 + l2)) \/ (Carrier l1)) \/ (Carrier l2)) \ (Carrier (l1 + l2)) by ;
then A37: not r /. k in Carrier (l1 + l2) by XBOOLE_0:def 5;
(ScFS (w,(l1 + l2),r)) . k = () . (w,(((l1 + l2) . (r /. k)) * (r /. k))) by ;
then (ScFS (w,(l1 + l2),r)) . k = () . (w,(() * (r /. k))) by A37
.= () . (w,(0. ())) by VECTSP_1:14
.= 0. F_Real by ZMODLAT2:14 ;
hence (ScFS (w,(l1 + l2),r)) . k = - ((ScFS (w,(l1 + l2),r)) . k)
.= - ((ScFS (w,(l1 + l2),r)) /. k) by ;
:: thesis: verum
end;
then A38: Sum (ScFS (w,(l1 + l2),r)) = - (Sum (ScFS (w,(l1 + l2),r))) by ;
A39: len p = len (ScFS (w,l1,p)) by defScFSDM;
B1: dom p = Seg (len p) by FINSEQ_1:def 3
.= Seg (len (ScFS (w,l1,p))) by defScFSDM
.= dom (ScFS (w,l1,p)) by FINSEQ_1:def 3 ;
now :: thesis: for k being Nat st k in dom (ScFS (w,l1,p)) holds
(ScFS (w,l1,p)) . k = - ((ScFS (w,l1,p)) /. k)
let k be Nat; :: thesis: ( k in dom (ScFS (w,l1,p)) implies (ScFS (w,l1,p)) . k = - ((ScFS (w,l1,p)) /. k) )
assume A40: k in dom (ScFS (w,l1,p)) ; :: thesis: (ScFS (w,l1,p)) . k = - ((ScFS (w,l1,p)) /. k)
then p /. k = p . k by ;
then p /. k in (((Carrier (l1 + l2)) \/ (Carrier l1)) \/ (Carrier l2)) \ (Carrier l1) by ;
then A41: not p /. k in Carrier l1 by XBOOLE_0:def 5;
(ScFS (w,l1,p)) . k = () . (w,((l1 . (p /. k)) * (p /. k))) by ;
then (ScFS (w,l1,p)) . k = () . (w,(() * (p /. k))) by A41
.= () . (w,(0. ())) by VECTSP_1:14
.= 0. F_Real by ZMODLAT2:14 ;
hence (ScFS (w,l1,p)) . k = - ((ScFS (w,l1,p)) . k)
.= - ((ScFS (w,l1,p)) /. k) by ;
:: thesis: verum
end;
then A42: Sum (ScFS (w,l1,p)) = - (Sum (ScFS (w,l1,p))) by ;
A43: len q = len (ScFS (w,l2,q)) by defScFSDM;
then B1: dom q = dom (ScFS (w,l2,q)) by FINSEQ_3:29;
now :: thesis: for k being Nat st k in dom (ScFS (w,l2,q)) holds
(ScFS (w,l2,q)) . k = - ((ScFS (w,l2,q)) /. k)
let k be Nat; :: thesis: ( k in dom (ScFS (w,l2,q)) implies (ScFS (w,l2,q)) . k = - ((ScFS (w,l2,q)) /. k) )
assume A44: k in dom (ScFS (w,l2,q)) ; :: thesis: (ScFS (w,l2,q)) . k = - ((ScFS (w,l2,q)) /. k)
then q /. k = q . k by ;
then q /. k in (((Carrier (l1 + l2)) \/ (Carrier l1)) \/ (Carrier l2)) \ (Carrier l2) by ;
then A45: not q /. k in Carrier l2 by XBOOLE_0:def 5;
(ScFS (w,l2,q)) . k = () . (w,((l2 . (q /. k)) * (q /. k))) by ;
then (ScFS (w,l2,q)) . k = () . (w,(() * (q /. k))) by A45
.= () . (w,(0. ())) by VECTSP_1:14
.= 0. F_Real by ZMODLAT2:14 ;
hence (ScFS (w,l2,q)) . k = - ((ScFS (w,l2,q)) . k)
.= - ((ScFS (w,l2,q)) /. k) by ;
:: thesis: verum
end;
then A46: Sum (ScFS (w,l2,q)) = - (Sum (ScFS (w,l2,q))) by ;
set g = ScFS (w,l1,(G ^ p));
A47: len (ScFS (w,l1,(G ^ p))) = len (G ^ p) by defScFSDM;
then A48: Seg (len (G ^ p)) = dom (ScFS (w,l1,(G ^ p))) by FINSEQ_1:def 3;
set f = ScFS (w,(l1 + l2),(F ^ r));
consider H being FinSequence of () such that
A49: H is one-to-one and
A50: rng H = Carrier l2 and
A51: Sum (ScFS (w,l2,H)) = SumSc (w,l2) by defSumScDM;
set HH = H ^ q;
rng H misses rng q
proof
set x = the Element of (rng H) /\ (rng q);
assume not rng H misses rng q ; :: thesis: contradiction
then ( the Element of (rng H) /\ (rng q) in Carrier l2 & the Element of (rng H) /\ (rng q) in (((Carrier (l1 + l2)) \/ (Carrier l1)) \/ (Carrier l2)) \ (Carrier l2) ) by ;
hence contradiction by XBOOLE_0:def 5; :: thesis: verum
end;
then A52: H ^ q is one-to-one by ;
rng (H ^ q) = (rng H) \/ (rng q) by FINSEQ_1:31;
then rng (H ^ q) = (Carrier l2) \/ (((Carrier (l1 + l2)) \/ (Carrier l1)) \/ (Carrier l2)) by ;
then A53: rng (H ^ q) = ((Carrier (l1 + l2)) \/ (Carrier l1)) \/ (Carrier l2) by ;
then A54: len (G ^ p) = len (H ^ q) by ;
then B1: dom (G ^ p) = dom (H ^ q) by FINSEQ_3:29;
deffunc H2( Nat) -> set = (H ^ q) <- ((G ^ p) . \$1);
consider R being FinSequence such that
A55: len R = len (H ^ q) and
A56: for k being Nat st k in dom R holds
R . k = H2(k) from A57: dom R = dom (H ^ q) by ;
A58: now :: thesis: for x being object st x in dom (G ^ p) holds
(G ^ p) . x = (H ^ q) . (R . x)
let x be object ; :: thesis: ( x in dom (G ^ p) implies (G ^ p) . x = (H ^ q) . (R . x) )
assume A59: x in dom (G ^ p) ; :: thesis: (G ^ p) . x = (H ^ q) . (R . x)
then reconsider n = x as Element of NAT ;
(G ^ p) . n in rng (H ^ q) by ;
then A60: H ^ q just_once_values (G ^ p) . n by ;
(H ^ q) . (R . n) = (H ^ q) . ((H ^ q) <- ((G ^ p) . n)) by A56, A57, B1, A59
.= (G ^ p) . n by ;
hence (G ^ p) . x = (H ^ q) . (R . x) ; :: thesis: verum
end;
A61: rng R c= dom (H ^ q)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng R or x in dom (H ^ q) )
assume x in rng R ; :: thesis: x in dom (H ^ q)
then consider y being object such that
A62: y in dom R and
A63: R . y = x by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A62;
y in dom (G ^ p) by ;
then (G ^ p) . y in rng (H ^ q) by ;
then A64: H ^ q just_once_values (G ^ p) . y by ;
R . y = (H ^ q) <- ((G ^ p) . y) by ;
hence x in dom (H ^ q) by ; :: thesis: verum
end;
now :: thesis: for x being object holds
( ( x in dom (G ^ p) implies ( x in dom R & R . x in dom (H ^ q) ) ) & ( x in dom R & R . x in dom (H ^ q) implies x in dom (G ^ p) ) )
let x be object ; :: thesis: ( ( x in dom (G ^ p) implies ( x in dom R & R . x in dom (H ^ q) ) ) & ( x in dom R & R . x in dom (H ^ q) implies x in dom (G ^ p) ) )
thus ( x in dom (G ^ p) implies ( x in dom R & R . x in dom (H ^ q) ) ) :: thesis: ( x in dom R & R . x in dom (H ^ q) implies x in dom (G ^ p) )
proof
assume x in dom (G ^ p) ; :: thesis: ( x in dom R & R . x in dom (H ^ q) )
hence x in dom R by ; :: thesis: R . x in dom (H ^ q)
then R . x in rng R by FUNCT_1:def 3;
hence R . x in dom (H ^ q) by A61; :: thesis: verum
end;
assume ( x in dom R & R . x in dom (H ^ q) ) ; :: thesis: x in dom (G ^ p)
hence x in dom (G ^ p) by ; :: thesis: verum
end;
then A66: G ^ p = (H ^ q) * R by ;
dom (H ^ q) c= rng R
proof
set f = ((H ^ q) ") * (G ^ p);
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (H ^ q) or x in rng R )
assume A67: x in dom (H ^ q) ; :: thesis: x in rng R
dom ((H ^ q) ") = rng (G ^ p) by ;
then A68: rng (((H ^ q) ") * (G ^ p)) = rng ((H ^ q) ") by RELAT_1:28
.= dom (H ^ q) by ;
((H ^ q) ") * (G ^ p) = (((H ^ q) ") * (H ^ q)) * R by
.= (id (dom (H ^ q))) * R by
.= R by ;
hence x in rng R by ; :: thesis: verum
end;
then A69: dom (H ^ q) = rng R by A61;
set h = ScFS (w,l2,(H ^ q));
A70: Sum (ScFS (w,l2,(H ^ q))) = Sum ((ScFS (w,l2,H)) ^ (ScFS (w,l2,q))) by ThScFSDM6
.= (Sum (ScFS (w,l2,H))) + () by
.= Sum (ScFS (w,l2,H)) ;
A71: Sum (ScFS (w,l1,(G ^ p))) = Sum ((ScFS (w,l1,G)) ^ (ScFS (w,l1,p))) by ThScFSDM6
.= (Sum (ScFS (w,l1,G))) + () by
.= Sum (ScFS (w,l1,G)) ;
A72: dom P = dom (F ^ r) by ;
A73: P is one-to-one by ;
A74: dom R = dom (H ^ q) by ;
A75: R is one-to-one by ;
R is Function of (dom (H ^ q)),(dom (H ^ q)) by ;
then reconsider R = R as Permutation of (dom (H ^ q)) by ;
A76: len (ScFS (w,l2,(H ^ q))) = len (H ^ q) by defScFSDM;
then dom (ScFS (w,l2,(H ^ q))) = dom (H ^ q) by FINSEQ_3:29;
then reconsider R = R as Permutation of (dom (ScFS (w,l2,(H ^ q)))) ;
reconsider Hp = (ScFS (w,l2,(H ^ q))) * R as FinSequence of F_Real by FINSEQ_2:47;
A77: len Hp = len (G ^ p) by ;
reconsider P = P as Function of (dom (F ^ r)),(dom (F ^ r)) by ;
reconsider P = P as Permutation of (dom (F ^ r)) by ;
A78: len (ScFS (w,(l1 + l2),(F ^ r))) = len (F ^ r) by defScFSDM;
then dom (ScFS (w,(l1 + l2),(F ^ r))) = dom (F ^ r) by FINSEQ_3:29;
then reconsider P = P as Permutation of (dom (ScFS (w,(l1 + l2),(F ^ r)))) ;
reconsider Fp = (ScFS (w,(l1 + l2),(F ^ r))) * P as FinSequence of F_Real by FINSEQ_2:47;
A79: Sum (ScFS (w,(l1 + l2),(F ^ r))) = Sum ((ScFS (w,(l1 + l2),F)) ^ (ScFS (w,(l1 + l2),r))) by ThScFSDM6
.= (Sum (ScFS (w,(l1 + l2),F))) + () by
.= Sum (ScFS (w,(l1 + l2),F)) ;
deffunc H3( Nat) -> Element of the carrier of F_Real = ((ScFS (w,l1,(G ^ p))) /. \$1) + (Hp /. \$1);
consider I being FinSequence such that
A80: len I = len (G ^ p) and
A81: for k being Nat st k in dom I holds
I . k = H3(k) from A83: dom I = Seg (len (G ^ p)) by ;
rng I c= the carrier of F_Real
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng I or x in the carrier of F_Real )
assume x in rng I ; :: thesis: x in the carrier of F_Real
then consider y being object such that
A84: y in dom I and
A85: I . y = x by FUNCT_1:def 3;
reconsider y = y as Element of NAT by A84;
I . y = ((ScFS (w,l1,(G ^ p))) /. y) + (Hp /. y) by ;
hence x in the carrier of F_Real by A85; :: thesis: verum
end;
then reconsider I = I as FinSequence of F_Real by FINSEQ_1:def 4;
A86: len Fp = len I by ;
then X1: ( dom I = Seg (len I) & dom Fp = Seg (len I) ) by FINSEQ_1:def 3;
X2: dom Hp = Seg (len Hp) by FINSEQ_1:def 3
.= dom I by ;
X3: dom (H ^ q) = Seg (len (H ^ q)) by FINSEQ_1:def 3
.= dom I by ;
then X4: dom (G ^ p) = dom I by ;
X5: dom (ScFS (w,l1,(G ^ p))) = Seg (len (ScFS (w,l1,(G ^ p)))) by FINSEQ_1:def 3
.= dom I by ;
A87: now :: thesis: for k being Nat st k in dom I holds
I . k = Fp . k
let k be Nat; :: thesis: ( k in dom I implies I . k = Fp . k )
assume A88: k in dom I ; :: thesis: I . k = Fp . k
then A90: Hp /. k = ((ScFS (w,l2,(H ^ q))) * R) . k by
.= (ScFS (w,l2,(H ^ q))) . (R . k) by ;
set v = (G ^ p) /. k;
A91: Fp . k = (ScFS (w,(l1 + l2),(F ^ r))) . (P . k) by ;
R . k in dom R by ;
then reconsider j = R . k as Element of NAT by FINSEQ_3:23;
A94: (H ^ q) . j = (G ^ p) . k by A58, A88, X3, B1
.= (G ^ p) /. k by ;
A95: dom (F ^ r) = dom (G ^ p) by ;
then P . k in dom P by ;
then reconsider l = P . k as Element of NAT by FINSEQ_3:23;
A96: (F ^ r) . l = (G ^ p) . k by A23, A88, X3, B1
.= (G ^ p) /. k by ;
R . k in dom (H ^ q) by ;
then A97: (ScFS (w,l2,(H ^ q))) . j = () . (w,((l2 . ((G ^ p) /. k)) * ((G ^ p) /. k))) by ;
P . k in dom (F ^ r) by ;
then A98: (ScFS (w,(l1 + l2),(F ^ r))) . l = () . (w,(((l1 + l2) . ((G ^ p) /. k)) * ((G ^ p) /. k))) by
.= () . (w,(((l1 . ((G ^ p) /. k)) + (l2 . ((G ^ p) /. k))) * ((G ^ p) /. k))) by VECTSP_6:22
.= () . (w,(((l1 . ((G ^ p) /. k)) * ((G ^ p) /. k)) + ((l2 . ((G ^ p) /. k)) * ((G ^ p) /. k)))) by VECTSP_1:def 15
.= (() . (w,((l1 . ((G ^ p) /. k)) * ((G ^ p) /. k)))) + (() . (w,((l2 . ((G ^ p) /. k)) * ((G ^ p) /. k)))) by ZMODLAT2:12 ;
(ScFS (w,l1,(G ^ p))) /. k = (ScFS (w,l1,(G ^ p))) . k by
.= () . (w,((l1 . ((G ^ p) /. k)) * ((G ^ p) /. k))) by ;
hence I . k = Fp . k by A81, A88, A90, A97, A91, A98; :: thesis: verum
end;
( dom I = Seg (len I) & dom Fp = Seg (len I) ) by ;
then A100: I = Fp by A87;
( Sum Fp = Sum (ScFS (w,(l1 + l2),(F ^ r))) & Sum Hp = Sum (ScFS (w,l2,(H ^ q))) ) by RLVECT_2:7;
hence SumSc (w,(l1 + l2)) = (SumSc (w,l1)) + (SumSc (w,l2)) by A11, A14, A47, A48, A51, A71, A70, A77, A79, A80, A81, A83, A100, RLVECT_2:2; :: thesis: verum