let L be Z_Lattice; :: thesis: for v being Vector of L

for l1, l2 being Linear_Combination of L holds SumSc (v,(l1 + l2)) = (SumSc (v,l1)) + (SumSc (v,l2))

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

let l1, l2 be Linear_Combination of 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 L by A1, FINSEQ_1:def 4;

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 L by A4, FINSEQ_1:def 4;

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 L by A7, FINSEQ_1:def 4;

consider F being FinSequence of L 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 defSumSc;

set FF = F ^ r;

consider G being FinSequence of L 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 defSumSc;

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 A10, A4, XBOOLE_1:39;

then A15: rng (F ^ r) = ((Carrier (l1 + l2)) \/ (Carrier l1)) \/ (Carrier l2) by A6, XBOOLE_1:7, XBOOLE_1:12;

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 A13, A1, XBOOLE_1:39;

then A16: rng (G ^ p) = ((Carrier (l1 + l2)) \/ (Carrier l1)) \/ (Carrier l2) by A3, XBOOLE_1:7, XBOOLE_1:12;

rng F misses rng r

rng G misses rng p

then A19: len (G ^ p) = len (F ^ r) by A17, A16, A15, FINSEQ_1:48;

deffunc H_{1}( 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 = H_{1}(k)
from FINSEQ_1:sch 2();

A22: dom P = dom (F ^ r) by A20, FINSEQ_3:29;

a22: dom (F ^ r) = dom (G ^ p) by A19, FINSEQ_3:29;

dom (F ^ r) c= rng P

A35: len r = len (ScFS (w,(l1 + l2),r)) by defScFS;

then B1: dom r = dom (ScFS (w,(l1 + l2),r)) by FINSEQ_3:29;

A39: len p = len (ScFS (w,l1,p)) by defScFS;

then B1: dom p = dom (ScFS (w,l1,p)) by FINSEQ_3:29;

A43: len q = len (ScFS (w,l2,q)) by defScFS;

then B1: dom q = dom (ScFS (w,l2,q)) by FINSEQ_3:29;

set g = ScFS (w,l1,(G ^ p));

A47: len (ScFS (w,l1,(G ^ p))) = len (G ^ p) by defScFS;

then A48: dom (G ^ p) = dom (ScFS (w,l1,(G ^ p))) by FINSEQ_3:29;

set f = ScFS (w,(l1 + l2),(F ^ r));

consider H being FinSequence of L 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 defSumSc;

set HH = H ^ q;

rng H misses rng q

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 A50, A7, XBOOLE_1:39;

then A53: rng (H ^ q) = ((Carrier (l1 + l2)) \/ (Carrier l1)) \/ (Carrier l2) by XBOOLE_1:7, XBOOLE_1:12;

then A54: len (G ^ p) = len (H ^ q) by A52, A18, A16, FINSEQ_1:48;

then a54: dom (G ^ p) = dom (H ^ q) by FINSEQ_3:29;

deffunc H_{2}( 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 = H_{2}(k)
from FINSEQ_1:sch 2();

A57: dom R = dom (H ^ q) by A55, FINSEQ_3:29;

dom (H ^ q) c= rng R

set h = ScFS (w,l2,(H ^ q));

A70: Sum (ScFS (w,l2,(H ^ q))) = Sum ((ScFS (w,l2,H)) ^ (ScFS (w,l2,q))) by ThScFS6

.= (Sum (ScFS (w,l2,H))) + (0. F_Real) by A46, RLVECT_1:41

.= Sum (ScFS (w,l2,H)) ;

A71: Sum (ScFS (w,l1,(G ^ p))) = Sum ((ScFS (w,l1,G)) ^ (ScFS (w,l1,p))) by ThScFS6

.= (Sum (ScFS (w,l1,G))) + (0. F_Real) by A42, RLVECT_1:41

.= Sum (ScFS (w,l1,G)) ;

A72: dom P = dom (F ^ r) by A20, FINSEQ_3:29;

A73: P is one-to-one by A20, A34, FINSEQ_3:29, FINSEQ_4:60;

A74: dom R = dom (H ^ q) by A55, FINSEQ_3:29;

A75: R is one-to-one by A55, A69, FINSEQ_3:29, FINSEQ_4:60;

R is Function of (dom (H ^ q)),(dom (H ^ q)) by A61, A74, FUNCT_2:2;

then reconsider R = R as Permutation of (dom (H ^ q)) by A69, A75, FUNCT_2:57;

A76: len (ScFS (w,l2,(H ^ q))) = len (H ^ q) by defScFS;

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 A54, A76, FINSEQ_2:44;

P is Function of (dom (F ^ r)),(dom (F ^ r)) by A26, A72, FUNCT_2:2;

then reconsider P = P as Permutation of (dom (F ^ r)) by A34, A73, FUNCT_2:57;

A78: len (ScFS (w,(l1 + l2),(F ^ r))) = len (F ^ r) by defScFS;

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 ThScFS6

.= (Sum (ScFS (w,(l1 + l2),F))) + (0. F_Real) by A38, RLVECT_1:41

.= Sum (ScFS (w,(l1 + l2),F)) ;

deffunc H_{3}( 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 = H_{3}(k)
from FINSEQ_1:sch 2();

A83: dom I = dom (G ^ p) by A80, FINSEQ_3:29;

rng I c= the carrier of F_Real

A86: len Fp = len I by A19, A78, A80, FINSEQ_2:44;

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 A54, A76, A80, FINSEQ_1:def 3, FINSEQ_2:44 ;

X3: dom (H ^ q) = Seg (len (H ^ q)) by FINSEQ_1:def 3

.= dom I by A18, A16, A52, A53, A80, FINSEQ_1:48, FINSEQ_1:def 3 ;

X5: dom (ScFS (w,l1,(G ^ p))) = Seg (len (ScFS (w,l1,(G ^ p)))) by FINSEQ_1:def 3

.= dom I by A80, defScFS, FINSEQ_1:def 3 ;

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, A51, A71, A70, A79, A80, A81, A83, A77, A47, A100, A48, RLVECT_2:2; :: thesis: verum

for l1, l2 being Linear_Combination of L holds SumSc (v,(l1 + l2)) = (SumSc (v,l1)) + (SumSc (v,l2))

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

let l1, l2 be Linear_Combination of 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 L by A1, FINSEQ_1:def 4;

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 L by A4, FINSEQ_1:def 4;

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 L by A7, FINSEQ_1:def 4;

consider F being FinSequence of L 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 defSumSc;

set FF = F ^ r;

consider G being FinSequence of L 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 defSumSc;

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 A10, A4, XBOOLE_1:39;

then A15: rng (F ^ r) = ((Carrier (l1 + l2)) \/ (Carrier l1)) \/ (Carrier l2) by A6, XBOOLE_1:7, XBOOLE_1:12;

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 A13, A1, XBOOLE_1:39;

then A16: rng (G ^ p) = ((Carrier (l1 + l2)) \/ (Carrier l1)) \/ (Carrier l2) by A3, XBOOLE_1:7, XBOOLE_1:12;

rng F misses rng r

proof

then A17:
F ^ r is one-to-one
by A9, A5, FINSEQ_3:91;
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 A10, A4, XBOOLE_0:def 4;

hence contradiction by XBOOLE_0:def 5; :: thesis: verum

end;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 A10, A4, XBOOLE_0:def 4;

hence contradiction by XBOOLE_0:def 5; :: thesis: verum

rng G misses rng p

proof

then A18:
G ^ p is one-to-one
by A12, A2, FINSEQ_3:91;
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 A13, A1, XBOOLE_0:def 4;

hence contradiction by XBOOLE_0:def 5; :: thesis: verum

end;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 A13, A1, XBOOLE_0:def 4;

hence contradiction by XBOOLE_0:def 5; :: thesis: verum

then A19: len (G ^ p) = len (F ^ r) by A17, A16, A15, FINSEQ_1:48;

deffunc H

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 = H

A22: dom P = dom (F ^ r) by A20, FINSEQ_3:29;

a22: dom (F ^ r) = dom (G ^ p) by A19, FINSEQ_3:29;

A23: now :: thesis: for x being object st x in dom (G ^ p) holds

(G ^ p) . x = (F ^ r) . (P . x)

A26:
rng P c= dom (F ^ r)
(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 A16, A15, A24, FUNCT_1:def 3;

then A25: F ^ r just_once_values (G ^ p) . n by A17, FINSEQ_4:8;

(F ^ r) . (P . n) = (F ^ r) . ((F ^ r) <- ((G ^ p) . n)) by A21, A22, a22, A24

.= (G ^ p) . n by A25, FINSEQ_4:def 3 ;

hence (G ^ p) . x = (F ^ r) . (P . x) ; :: thesis: verum

end;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 A16, A15, A24, FUNCT_1:def 3;

then A25: F ^ r just_once_values (G ^ p) . n by A17, FINSEQ_4:8;

(F ^ r) . (P . n) = (F ^ r) . ((F ^ r) <- ((G ^ p) . n)) by A21, A22, a22, A24

.= (G ^ p) . n by A25, FINSEQ_4:def 3 ;

hence (G ^ p) . x = (F ^ r) . (P . x) ; :: thesis: verum

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 A19, A20, A27, FINSEQ_3:29;

then (G ^ p) . y in rng (F ^ r) by A16, A15, FUNCT_1:def 3;

then A29: F ^ r just_once_values (G ^ p) . y by A17, FINSEQ_4:8;

P . y = (F ^ r) <- ((G ^ p) . y) by A21, A27;

hence x in dom (F ^ r) by A28, A29, FINSEQ_4:def 3; :: thesis: verum

end;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 A19, A20, A27, FINSEQ_3:29;

then (G ^ p) . y in rng (F ^ r) by A16, A15, FUNCT_1:def 3;

then A29: F ^ r just_once_values (G ^ p) . y by A17, FINSEQ_4:8;

P . y = (F ^ r) <- ((G ^ p) . y) by A21, A27;

hence x in dom (F ^ r) by A28, A29, FINSEQ_4:def 3; :: thesis: verum

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

then A31:
G ^ p = (F ^ r) * P
by A23, FUNCT_1:10;( ( 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) )

hence x in dom (G ^ p) by A20, FINSEQ_3:29, A19; :: thesis: verum

end;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 P & P . x in dom (F ^ r) )
; :: thesis: x in dom (G ^ p)
assume
x in dom (G ^ p)
; :: thesis: ( x in dom P & P . x in dom (F ^ r) )

hence x in dom P by A20, FINSEQ_3:29, A19; :: 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;hence x in dom P by A20, FINSEQ_3:29, A19; :: 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

hence x in dom (G ^ p) by A20, FINSEQ_3:29, A19; :: thesis: verum

dom (F ^ r) c= rng P

proof

then A34:
dom (F ^ r) = rng P
by A26;
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 A17, A16, A15, FUNCT_1:33;

then A33: rng (((F ^ r) ") * (G ^ p)) = rng ((F ^ r) ") by RELAT_1:28

.= dom (F ^ r) by A17, FUNCT_1:33 ;

((F ^ r) ") * (G ^ p) = (((F ^ r) ") * (F ^ r)) * P by A31, RELAT_1:36

.= (id (dom (F ^ r))) * P by A17, FUNCT_1:39

.= P by A26, RELAT_1:53 ;

hence x in rng P by A32, A33; :: thesis: verum

end;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 A17, A16, A15, FUNCT_1:33;

then A33: rng (((F ^ r) ") * (G ^ p)) = rng ((F ^ r) ") by RELAT_1:28

.= dom (F ^ r) by A17, FUNCT_1:33 ;

((F ^ r) ") * (G ^ p) = (((F ^ r) ") * (F ^ r)) * P by A31, RELAT_1:36

.= (id (dom (F ^ r))) * P by A17, FUNCT_1:39

.= P by A26, RELAT_1:53 ;

hence x in rng P by A32, A33; :: thesis: verum

A35: len r = len (ScFS (w,(l1 + l2),r)) by defScFS;

then B1: dom r = dom (ScFS (w,(l1 + l2),r)) by FINSEQ_3:29;

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)

then A38:
Sum (ScFS (w,(l1 + l2),r)) = - (Sum (ScFS (w,(l1 + l2),r)))
by A35, RLVECT_2:4;(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 B1, PARTFUN1:def 6;

then r /. k in (((Carrier (l1 + l2)) \/ (Carrier l1)) \/ (Carrier l2)) \ (Carrier (l1 + l2)) by A4, A36, B1, FUNCT_1:def 3;

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 A36, defScFS;

then (ScFS (w,(l1 + l2),r)) . k = <;w,((0. INT.Ring) * (r /. k));> by A37

.= <;w,(0. L);> by VECTSP_1:14

.= 0. F_Real by ZMODLAT1:12 ;

hence (ScFS (w,(l1 + l2),r)) . k = - ((ScFS (w,(l1 + l2),r)) . k)

.= - ((ScFS (w,(l1 + l2),r)) /. k) by A36, PARTFUN1:def 6 ;

:: thesis: verum

end;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 B1, PARTFUN1:def 6;

then r /. k in (((Carrier (l1 + l2)) \/ (Carrier l1)) \/ (Carrier l2)) \ (Carrier (l1 + l2)) by A4, A36, B1, FUNCT_1:def 3;

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 A36, defScFS;

then (ScFS (w,(l1 + l2),r)) . k = <;w,((0. INT.Ring) * (r /. k));> by A37

.= <;w,(0. L);> by VECTSP_1:14

.= 0. F_Real by ZMODLAT1:12 ;

hence (ScFS (w,(l1 + l2),r)) . k = - ((ScFS (w,(l1 + l2),r)) . k)

.= - ((ScFS (w,(l1 + l2),r)) /. k) by A36, PARTFUN1:def 6 ;

:: thesis: verum

A39: len p = len (ScFS (w,l1,p)) by defScFS;

then B1: dom p = dom (ScFS (w,l1,p)) by FINSEQ_3:29;

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)

then A42:
Sum (ScFS (w,l1,p)) = - (Sum (ScFS (w,l1,p)))
by A39, RLVECT_2:4;(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 B1, PARTFUN1:def 6;

then p /. k in (((Carrier (l1 + l2)) \/ (Carrier l1)) \/ (Carrier l2)) \ (Carrier l1) by A1, A40, B1, FUNCT_1:def 3;

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 A40, defScFS;

then (ScFS (w,l1,p)) . k = <;w,((0. INT.Ring) * (p /. k));> by A41

.= <;w,(0. L);> by VECTSP_1:14

.= 0. F_Real by ZMODLAT1:12 ;

hence (ScFS (w,l1,p)) . k = - ((ScFS (w,l1,p)) . k)

.= - ((ScFS (w,l1,p)) /. k) by A40, PARTFUN1:def 6 ;

:: thesis: verum

end;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 B1, PARTFUN1:def 6;

then p /. k in (((Carrier (l1 + l2)) \/ (Carrier l1)) \/ (Carrier l2)) \ (Carrier l1) by A1, A40, B1, FUNCT_1:def 3;

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 A40, defScFS;

then (ScFS (w,l1,p)) . k = <;w,((0. INT.Ring) * (p /. k));> by A41

.= <;w,(0. L);> by VECTSP_1:14

.= 0. F_Real by ZMODLAT1:12 ;

hence (ScFS (w,l1,p)) . k = - ((ScFS (w,l1,p)) . k)

.= - ((ScFS (w,l1,p)) /. k) by A40, PARTFUN1:def 6 ;

:: thesis: verum

A43: len q = len (ScFS (w,l2,q)) by defScFS;

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)

then A46:
Sum (ScFS (w,l2,q)) = - (Sum (ScFS (w,l2,q)))
by A43, RLVECT_2:4;(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 B1, PARTFUN1:def 6;

then q /. k in (((Carrier (l1 + l2)) \/ (Carrier l1)) \/ (Carrier l2)) \ (Carrier l2) by A7, A44, B1, FUNCT_1:def 3;

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 A44, defScFS;

then (ScFS (w,l2,q)) . k = <;w,((0. INT.Ring) * (q /. k));> by A45

.= <;w,(0. L);> by VECTSP_1:14

.= 0. F_Real by ZMODLAT1:12 ;

hence (ScFS (w,l2,q)) . k = - ((ScFS (w,l2,q)) . k)

.= - ((ScFS (w,l2,q)) /. k) by A44, PARTFUN1:def 6 ;

:: thesis: verum

end;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 B1, PARTFUN1:def 6;

then q /. k in (((Carrier (l1 + l2)) \/ (Carrier l1)) \/ (Carrier l2)) \ (Carrier l2) by A7, A44, B1, FUNCT_1:def 3;

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 A44, defScFS;

then (ScFS (w,l2,q)) . k = <;w,((0. INT.Ring) * (q /. k));> by A45

.= <;w,(0. L);> by VECTSP_1:14

.= 0. F_Real by ZMODLAT1:12 ;

hence (ScFS (w,l2,q)) . k = - ((ScFS (w,l2,q)) . k)

.= - ((ScFS (w,l2,q)) /. k) by A44, PARTFUN1:def 6 ;

:: thesis: verum

set g = ScFS (w,l1,(G ^ p));

A47: len (ScFS (w,l1,(G ^ p))) = len (G ^ p) by defScFS;

then A48: dom (G ^ p) = dom (ScFS (w,l1,(G ^ p))) by FINSEQ_3:29;

set f = ScFS (w,(l1 + l2),(F ^ r));

consider H being FinSequence of L 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 defSumSc;

set HH = H ^ q;

rng H misses rng q

proof

then A52:
H ^ q is one-to-one
by A49, A8, FINSEQ_3:91;
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 A50, A7, XBOOLE_0:def 4;

hence contradiction by XBOOLE_0:def 5; :: thesis: verum

end;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 A50, A7, XBOOLE_0:def 4;

hence contradiction by XBOOLE_0:def 5; :: thesis: verum

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 A50, A7, XBOOLE_1:39;

then A53: rng (H ^ q) = ((Carrier (l1 + l2)) \/ (Carrier l1)) \/ (Carrier l2) by XBOOLE_1:7, XBOOLE_1:12;

then A54: len (G ^ p) = len (H ^ q) by A52, A18, A16, FINSEQ_1:48;

then a54: dom (G ^ p) = dom (H ^ q) by FINSEQ_3:29;

deffunc H

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 = H

A57: dom R = dom (H ^ q) by A55, FINSEQ_3:29;

A58: now :: thesis: for x being object st x in dom (G ^ p) holds

(G ^ p) . x = (H ^ q) . (R . x)

A61:
rng R c= dom (H ^ q)
(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 A16, A53, A59, FUNCT_1:def 3;

then A60: H ^ q just_once_values (G ^ p) . n by A52, FINSEQ_4:8;

(H ^ q) . (R . n) = (H ^ q) . ((H ^ q) <- ((G ^ p) . n)) by A56, A57, A59, a54

.= (G ^ p) . n by A60, FINSEQ_4:def 3 ;

hence (G ^ p) . x = (H ^ q) . (R . x) ; :: thesis: verum

end;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 A16, A53, A59, FUNCT_1:def 3;

then A60: H ^ q just_once_values (G ^ p) . n by A52, FINSEQ_4:8;

(H ^ q) . (R . n) = (H ^ q) . ((H ^ q) <- ((G ^ p) . n)) by A56, A57, A59, a54

.= (G ^ p) . n by A60, FINSEQ_4:def 3 ;

hence (G ^ p) . x = (H ^ q) . (R . x) ; :: thesis: verum

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 A54, A55, A62, FINSEQ_3:29;

then (G ^ p) . y in rng (H ^ q) by A16, A53, FUNCT_1:def 3;

then A64: H ^ q just_once_values (G ^ p) . y by A52, FINSEQ_4:8;

R . y = (H ^ q) <- ((G ^ p) . y) by A56, A62;

hence x in dom (H ^ q) by A63, A64, FINSEQ_4:def 3; :: thesis: verum

end;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 A54, A55, A62, FINSEQ_3:29;

then (G ^ p) . y in rng (H ^ q) by A16, A53, FUNCT_1:def 3;

then A64: H ^ q just_once_values (G ^ p) . y by A52, FINSEQ_4:8;

R . y = (H ^ q) <- ((G ^ p) . y) by A56, A62;

hence x in dom (H ^ q) by A63, A64, FINSEQ_4:def 3; :: thesis: verum

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

then A66:
G ^ p = (H ^ q) * R
by A58, FUNCT_1:10;( ( 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) )

hence x in dom (G ^ p) by A54, A55, FINSEQ_3:29; :: thesis: verum

end;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 R & R . x in dom (H ^ q) )
; :: thesis: x in dom (G ^ p)
assume
x in dom (G ^ p)
; :: thesis: ( x in dom R & R . x in dom (H ^ q) )

hence x in dom R by A55, FINSEQ_3:29, A54; :: 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;hence x in dom R by A55, FINSEQ_3:29, A54; :: 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

hence x in dom (G ^ p) by A54, A55, FINSEQ_3:29; :: thesis: verum

dom (H ^ q) c= rng R

proof

then A69:
dom (H ^ q) = rng R
by A61;
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 A52, A16, A53, FUNCT_1:33;

then A68: rng (((H ^ q) ") * (G ^ p)) = rng ((H ^ q) ") by RELAT_1:28

.= dom (H ^ q) by A52, FUNCT_1:33 ;

((H ^ q) ") * (G ^ p) = (((H ^ q) ") * (H ^ q)) * R by A66, RELAT_1:36

.= (id (dom (H ^ q))) * R by A52, FUNCT_1:39

.= R by A61, RELAT_1:53 ;

hence x in rng R by A67, A68; :: thesis: verum

end;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 A52, A16, A53, FUNCT_1:33;

then A68: rng (((H ^ q) ") * (G ^ p)) = rng ((H ^ q) ") by RELAT_1:28

.= dom (H ^ q) by A52, FUNCT_1:33 ;

((H ^ q) ") * (G ^ p) = (((H ^ q) ") * (H ^ q)) * R by A66, RELAT_1:36

.= (id (dom (H ^ q))) * R by A52, FUNCT_1:39

.= R by A61, RELAT_1:53 ;

hence x in rng R by A67, A68; :: thesis: verum

set h = ScFS (w,l2,(H ^ q));

A70: Sum (ScFS (w,l2,(H ^ q))) = Sum ((ScFS (w,l2,H)) ^ (ScFS (w,l2,q))) by ThScFS6

.= (Sum (ScFS (w,l2,H))) + (0. F_Real) by A46, RLVECT_1:41

.= Sum (ScFS (w,l2,H)) ;

A71: Sum (ScFS (w,l1,(G ^ p))) = Sum ((ScFS (w,l1,G)) ^ (ScFS (w,l1,p))) by ThScFS6

.= (Sum (ScFS (w,l1,G))) + (0. F_Real) by A42, RLVECT_1:41

.= Sum (ScFS (w,l1,G)) ;

A72: dom P = dom (F ^ r) by A20, FINSEQ_3:29;

A73: P is one-to-one by A20, A34, FINSEQ_3:29, FINSEQ_4:60;

A74: dom R = dom (H ^ q) by A55, FINSEQ_3:29;

A75: R is one-to-one by A55, A69, FINSEQ_3:29, FINSEQ_4:60;

R is Function of (dom (H ^ q)),(dom (H ^ q)) by A61, A74, FUNCT_2:2;

then reconsider R = R as Permutation of (dom (H ^ q)) by A69, A75, FUNCT_2:57;

A76: len (ScFS (w,l2,(H ^ q))) = len (H ^ q) by defScFS;

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 A54, A76, FINSEQ_2:44;

P is Function of (dom (F ^ r)),(dom (F ^ r)) by A26, A72, FUNCT_2:2;

then reconsider P = P as Permutation of (dom (F ^ r)) by A34, A73, FUNCT_2:57;

A78: len (ScFS (w,(l1 + l2),(F ^ r))) = len (F ^ r) by defScFS;

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 ThScFS6

.= (Sum (ScFS (w,(l1 + l2),F))) + (0. F_Real) by A38, RLVECT_1:41

.= Sum (ScFS (w,(l1 + l2),F)) ;

deffunc H

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 = H

A83: dom I = dom (G ^ p) by A80, FINSEQ_3:29;

rng I c= the carrier of F_Real

proof

then reconsider I = I as FinSequence of F_Real by FINSEQ_1:def 4;
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 A81, A84;

hence x in the carrier of F_Real by A85; :: thesis: verum

end;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 A81, A84;

hence x in the carrier of F_Real by A85; :: thesis: verum

A86: len Fp = len I by A19, A78, A80, FINSEQ_2:44;

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 A54, A76, A80, FINSEQ_1:def 3, FINSEQ_2:44 ;

X3: dom (H ^ q) = Seg (len (H ^ q)) by FINSEQ_1:def 3

.= dom I by A18, A16, A52, A53, A80, FINSEQ_1:48, FINSEQ_1:def 3 ;

X5: dom (ScFS (w,l1,(G ^ p))) = Seg (len (ScFS (w,l1,(G ^ p)))) by FINSEQ_1:def 3

.= dom I by A80, defScFS, FINSEQ_1:def 3 ;

A87: now :: thesis: for k being Nat st k in dom I holds

I . k = Fp . k

( dom I = Seg (len I) & dom Fp = Seg (len I) )
by A86, FINSEQ_1:def 3;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 X2, PARTFUN1:def 6

.= (ScFS (w,l2,(H ^ q))) . (R . k) by A88, X2, FUNCT_1:12 ;

set v = (G ^ p) /. k;

A91: Fp . k = (ScFS (w,(l1 + l2),(F ^ r))) . (P . k) by A88, X1, FUNCT_1:12;

R . k in dom R by A69, A74, A88, X3, FUNCT_1:def 3;

then reconsider j = R . k as Element of NAT by FINSEQ_3:23;

A94: (H ^ q) . j = (G ^ p) . k by A58, A88, X3, a54

.= (G ^ p) /. k by A88, X3, PARTFUN1:def 6, a54 ;

A95: dom (F ^ r) = dom (G ^ p) by A19, FINSEQ_3:29;

then P . k in dom P by A34, A72, A88, X3, FUNCT_1:def 3, a54;

then reconsider l = P . k as Element of NAT by FINSEQ_3:23;

A96: (F ^ r) . l = (G ^ p) . k by A23, A88, X3, a54

.= (G ^ p) /. k by A88, X3, a54, PARTFUN1:def 6 ;

R . k in dom (H ^ q) by A69, A74, A88, X3, FUNCT_1:def 3;

then A97: (ScFS (w,l2,(H ^ q))) . j = <;w,((l2 . ((G ^ p) /. k)) * ((G ^ p) /. k));> by A94, ThScFS1;

P . k in dom (F ^ r) by A34, A72, A88, A95, X3, a54, FUNCT_1:def 3;

then A98: (ScFS (w,(l1 + l2),(F ^ r))) . l = <;w,(((l1 + l2) . ((G ^ p) /. k)) * ((G ^ p) /. k));> by A96, ThScFS1

.= <;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 ZMODLAT1:8 ;

(ScFS (w,l1,(G ^ p))) /. k = (ScFS (w,l1,(G ^ p))) . k by A88, X5, PARTFUN1:def 6

.= <;w,((l1 . ((G ^ p) /. k)) * ((G ^ p) /. k));> by A88, X5, defScFS ;

hence I . k = Fp . k by A81, A88, A90, A97, A91, A98; :: thesis: verum

end;assume A88: k in dom I ; :: thesis: I . k = Fp . k

then A90: Hp /. k = ((ScFS (w,l2,(H ^ q))) * R) . k by X2, PARTFUN1:def 6

.= (ScFS (w,l2,(H ^ q))) . (R . k) by A88, X2, FUNCT_1:12 ;

set v = (G ^ p) /. k;

A91: Fp . k = (ScFS (w,(l1 + l2),(F ^ r))) . (P . k) by A88, X1, FUNCT_1:12;

R . k in dom R by A69, A74, A88, X3, FUNCT_1:def 3;

then reconsider j = R . k as Element of NAT by FINSEQ_3:23;

A94: (H ^ q) . j = (G ^ p) . k by A58, A88, X3, a54

.= (G ^ p) /. k by A88, X3, PARTFUN1:def 6, a54 ;

A95: dom (F ^ r) = dom (G ^ p) by A19, FINSEQ_3:29;

then P . k in dom P by A34, A72, A88, X3, FUNCT_1:def 3, a54;

then reconsider l = P . k as Element of NAT by FINSEQ_3:23;

A96: (F ^ r) . l = (G ^ p) . k by A23, A88, X3, a54

.= (G ^ p) /. k by A88, X3, a54, PARTFUN1:def 6 ;

R . k in dom (H ^ q) by A69, A74, A88, X3, FUNCT_1:def 3;

then A97: (ScFS (w,l2,(H ^ q))) . j = <;w,((l2 . ((G ^ p) /. k)) * ((G ^ p) /. k));> by A94, ThScFS1;

P . k in dom (F ^ r) by A34, A72, A88, A95, X3, a54, FUNCT_1:def 3;

then A98: (ScFS (w,(l1 + l2),(F ^ r))) . l = <;w,(((l1 + l2) . ((G ^ p) /. k)) * ((G ^ p) /. k));> by A96, ThScFS1

.= <;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 ZMODLAT1:8 ;

(ScFS (w,l1,(G ^ p))) /. k = (ScFS (w,l1,(G ^ p))) . k by A88, X5, PARTFUN1:def 6

.= <;w,((l1 . ((G ^ p) /. k)) * ((G ^ p) /. k));> by A88, X5, defScFS ;

hence I . k = Fp . k by A81, A88, A90, A97, A91, A98; :: thesis: verum

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, A51, A71, A70, A79, A80, A81, A83, A77, A47, A100, A48, RLVECT_2:2; :: thesis: verum