let V be RealLinearSpace; :: thesis: for L1, L2 being Linear_Combination of V holds Sum (L1 + L2) = (Sum L1) + (Sum L2)

let L1, L2 be Linear_Combination of V; :: thesis: Sum (L1 + L2) = (Sum L1) + (Sum L2)

consider F being FinSequence of the carrier of V such that

A1: F is one-to-one and

A2: rng F = Carrier (L1 + L2) and

A3: Sum ((L1 + L2) (#) F) = Sum (L1 + L2) by RLVECT_2:def 8;

set A = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2);

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 the carrier of V by A4, FINSEQ_1:def 4;

set FF = F ^ r;

A6: ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) = (Carrier (L1 + L2)) \/ ((Carrier L1) \/ (Carrier L2)) by XBOOLE_1:4;

rng F misses rng r

A8: len r = len ((L1 + L2) (#) r) by RLVECT_2:def 7;

.= 0. V by RLVECT_1:10 ;

set f = (L1 + L2) (#) (F ^ r);

set C1 = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L1);

consider G being FinSequence of the carrier of V such that

A12: G is one-to-one and

A13: rng G = Carrier L1 and

A14: Sum (L1 (#) G) = Sum L1 by RLVECT_2:def 8;

consider p being FinSequence such that

A15: rng p = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L1) and

A16: p is one-to-one by FINSEQ_4:58;

reconsider p = p as FinSequence of the carrier of V by A15, FINSEQ_1:def 4;

set GG = G ^ p;

A17: Sum ((L1 + L2) (#) (F ^ r)) = Sum (((L1 + L2) (#) F) ^ ((L1 + L2) (#) r)) by Lm1

.= (Sum ((L1 + L2) (#) F)) + (0. V) by A11, RLVECT_1:41

.= Sum ((L1 + L2) (#) F) ;

set C2 = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2);

consider H being FinSequence of the carrier of V such that

A18: H is one-to-one and

A19: rng H = Carrier L2 and

A20: Sum (L2 (#) H) = Sum L2 by RLVECT_2:def 8;

consider q being FinSequence such that

A21: rng q = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2) and

A22: q is one-to-one by FINSEQ_4:58;

reconsider q = q as FinSequence of the carrier of V by A21, FINSEQ_1:def 4;

set HH = H ^ q;

rng H misses rng q

set h = L2 (#) (H ^ q);

A24: ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) = (Carrier L1) \/ ((Carrier (L1 + L2)) \/ (Carrier L2)) by XBOOLE_1:4;

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

then A25: rng (G ^ p) = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) by A24, XBOOLE_1:7, XBOOLE_1:12;

A26: len q = len (L2 (#) q) by RLVECT_2:def 7;

.= 0. V by RLVECT_1:10 ;

A30: Sum (L2 (#) (H ^ q)) = Sum ((L2 (#) H) ^ (L2 (#) q)) by Lm1

.= (Sum (L2 (#) H)) + (0. V) by A29, RLVECT_1:41

.= Sum (L2 (#) H) ;

deffunc H_{1}( Nat) -> set = (F ^ r) <- ((G ^ p) . $1);

set g = L1 (#) (G ^ p);

consider P being FinSequence such that

A31: len P = len (F ^ r) and

A32: for k being Nat st k in dom P holds

P . k = H_{1}(k)
from FINSEQ_1:sch 2();

A33: dom P = Seg (len (F ^ r)) by A31, FINSEQ_1:def 3;

A34: len p = len (L1 (#) p) by RLVECT_2:def 7;

.= 0. V by RLVECT_1:10 ;

A38: Sum (L1 (#) (G ^ p)) = Sum ((L1 (#) G) ^ (L1 (#) p)) by Lm1

.= (Sum (L1 (#) G)) + (0. V) by A37, RLVECT_1:41

.= Sum (L1 (#) G) ;

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

then A39: rng (F ^ r) = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) by A6, XBOOLE_1:7, XBOOLE_1:12;

rng G misses rng p

then A41: len (G ^ p) = len (F ^ r) by A7, A25, A39, FINSEQ_1:48;

A42: dom P = Seg (len (F ^ r)) by A31, FINSEQ_1:def 3;

Seg (len (F ^ r)) c= rng P

then A56: P is one-to-one by A33, FINSEQ_4:60;

reconsider P = P as Function of (Seg (len (F ^ r))),(Seg (len (F ^ r))) by A46, A33, FUNCT_2:2;

reconsider P = P as Permutation of (Seg (len (F ^ r))) by A55, A56, FUNCT_2:57;

A57: len ((L1 + L2) (#) (F ^ r)) = len (F ^ r) by RLVECT_2:def 7;

then A58: Seg (len (F ^ r)) = dom ((L1 + L2) (#) (F ^ r)) by FINSEQ_1:def 3;

then reconsider Fp = ((L1 + L2) (#) (F ^ r)) * P as FinSequence of the carrier of V by FINSEQ_2:47;

A59: len (L1 (#) (G ^ p)) = len (G ^ p) by RLVECT_2:def 7;

deffunc H_{2}( Nat) -> set = (H ^ q) <- ((G ^ p) . $1);

consider R being FinSequence such that

A60: len R = len (H ^ q) and

A61: for k being Nat st k in dom R holds

R . k = H_{2}(k)
from FINSEQ_1:sch 2();

A62: dom R = Seg (len (H ^ q)) by A60, FINSEQ_1:def 3;

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 A19, A21, XBOOLE_1:39;

then A63: rng (H ^ q) = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) by XBOOLE_1:7, XBOOLE_1:12;

then A64: len (G ^ p) = len (H ^ q) by A23, A40, A25, FINSEQ_1:48;

A65: dom R = Seg (len (H ^ q)) by A60, FINSEQ_1:def 3;

Seg (len (H ^ q)) c= rng R

then A79: R is one-to-one by A62, FINSEQ_4:60;

reconsider R = R as Function of (Seg (len (H ^ q))),(Seg (len (H ^ q))) by A69, A62, FUNCT_2:2;

reconsider R = R as Permutation of (Seg (len (H ^ q))) by A78, A79, FUNCT_2:57;

A80: len (L2 (#) (H ^ q)) = len (H ^ q) by RLVECT_2:def 7;

then A81: Seg (len (H ^ q)) = dom (L2 (#) (H ^ q)) by FINSEQ_1:def 3;

then reconsider Hp = (L2 (#) (H ^ q)) * R as FinSequence of the carrier of V by FINSEQ_2:47;

A82: len Hp = len (G ^ p) by A64, A80, A81, FINSEQ_2:44;

deffunc H_{3}( Nat) -> Element of the carrier of V = ((L1 (#) (G ^ p)) /. $1) + (Hp /. $1);

consider I being FinSequence such that

A83: len I = len (G ^ p) and

A84: for k being Nat st k in dom I holds

I . k = H_{3}(k)
from FINSEQ_1:sch 2();

dom I = Seg (len (G ^ p)) by A83, FINSEQ_1:def 3;

then A85: for k being Nat st k in Seg (len (G ^ p)) holds

I . k = H_{3}(k)
by A84;

rng I c= the carrier of V

A88: len Fp = len I by A41, A57, A58, A83, FINSEQ_2:44;

then A102: Sum Hp = Sum (L2 (#) (H ^ q)) by A80, RLVECT_2:7;

dom ((L1 + L2) (#) (F ^ r)) = Seg (len ((L1 + L2) (#) (F ^ r))) by FINSEQ_1:def 3;

then A103: Sum Fp = Sum ((L1 + L2) (#) (F ^ r)) by A57, RLVECT_2:7;

( dom I = Seg (len I) & dom Fp = Seg (len I) ) by A88, FINSEQ_1:def 3;

then A104: I = Fp by A89, FUNCT_1:2;

Seg (len (G ^ p)) = dom (L1 (#) (G ^ p)) by A59, FINSEQ_1:def 3;

hence Sum (L1 + L2) = (Sum L1) + (Sum L2) by A3, A14, A20, A38, A30, A17, A103, A102, A83, A85, A82, A59, A104, RLVECT_2:2; :: thesis: verum

let L1, L2 be Linear_Combination of V; :: thesis: Sum (L1 + L2) = (Sum L1) + (Sum L2)

consider F being FinSequence of the carrier of V such that

A1: F is one-to-one and

A2: rng F = Carrier (L1 + L2) and

A3: Sum ((L1 + L2) (#) F) = Sum (L1 + L2) by RLVECT_2:def 8;

set A = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2);

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 the carrier of V by A4, FINSEQ_1:def 4;

set FF = F ^ r;

A6: ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) = (Carrier (L1 + L2)) \/ ((Carrier L1) \/ (Carrier L2)) by XBOOLE_1:4;

rng F misses rng r

proof

then A7:
F ^ r is one-to-one
by A1, A5, FINSEQ_3:91;
set x = the Element of (rng F) /\ (rng r);

assume not rng F misses rng r ; :: thesis: contradiction

then (rng F) /\ (rng r) <> {} ;

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 A2, 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 (rng F) /\ (rng r) <> {} ;

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

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

A8: len r = len ((L1 + L2) (#) r) by RLVECT_2:def 7;

now :: thesis: for k being Nat st k in dom r holds

((L1 + L2) (#) r) . k = 0 * (r /. k)

then A11: Sum ((L1 + L2) (#) r) =
0 * (Sum r)
by A8, RLVECT_2:3
((L1 + L2) (#) r) . k = 0 * (r /. k)

let k be Nat; :: thesis: ( k in dom r implies ((L1 + L2) (#) r) . k = 0 * (r /. k) )

assume A9: k in dom r ; :: thesis: ((L1 + L2) (#) r) . k = 0 * (r /. k)

then r /. k = r . k by PARTFUN1:def 6;

then r /. k in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier (L1 + L2)) by A4, A9, FUNCT_1:def 3;

then A10: not r /. k in Carrier (L1 + L2) by XBOOLE_0:def 5;

k in dom ((L1 + L2) (#) r) by A8, A9, FINSEQ_3:29;

then ((L1 + L2) (#) r) . k = ((L1 + L2) . (r /. k)) * (r /. k) by RLVECT_2:def 7;

hence ((L1 + L2) (#) r) . k = 0 * (r /. k) by A10; :: thesis: verum

end;assume A9: k in dom r ; :: thesis: ((L1 + L2) (#) r) . k = 0 * (r /. k)

then r /. k = r . k by PARTFUN1:def 6;

then r /. k in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier (L1 + L2)) by A4, A9, FUNCT_1:def 3;

then A10: not r /. k in Carrier (L1 + L2) by XBOOLE_0:def 5;

k in dom ((L1 + L2) (#) r) by A8, A9, FINSEQ_3:29;

then ((L1 + L2) (#) r) . k = ((L1 + L2) . (r /. k)) * (r /. k) by RLVECT_2:def 7;

hence ((L1 + L2) (#) r) . k = 0 * (r /. k) by A10; :: thesis: verum

.= 0. V by RLVECT_1:10 ;

set f = (L1 + L2) (#) (F ^ r);

set C1 = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L1);

consider G being FinSequence of the carrier of V such that

A12: G is one-to-one and

A13: rng G = Carrier L1 and

A14: Sum (L1 (#) G) = Sum L1 by RLVECT_2:def 8;

consider p being FinSequence such that

A15: rng p = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L1) and

A16: p is one-to-one by FINSEQ_4:58;

reconsider p = p as FinSequence of the carrier of V by A15, FINSEQ_1:def 4;

set GG = G ^ p;

A17: Sum ((L1 + L2) (#) (F ^ r)) = Sum (((L1 + L2) (#) F) ^ ((L1 + L2) (#) r)) by Lm1

.= (Sum ((L1 + L2) (#) F)) + (0. V) by A11, RLVECT_1:41

.= Sum ((L1 + L2) (#) F) ;

set C2 = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2);

consider H being FinSequence of the carrier of V such that

A18: H is one-to-one and

A19: rng H = Carrier L2 and

A20: Sum (L2 (#) H) = Sum L2 by RLVECT_2:def 8;

consider q being FinSequence such that

A21: rng q = (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2) and

A22: q is one-to-one by FINSEQ_4:58;

reconsider q = q as FinSequence of the carrier of V by A21, FINSEQ_1:def 4;

set HH = H ^ q;

rng H misses rng q

proof

then A23:
H ^ q is one-to-one
by A18, A22, FINSEQ_3:91;
set x = the Element of (rng H) /\ (rng q);

assume not rng H misses rng q ; :: thesis: contradiction

then (rng H) /\ (rng q) <> {} ;

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 A19, A21, XBOOLE_0:def 4;

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

end;assume not rng H misses rng q ; :: thesis: contradiction

then (rng H) /\ (rng q) <> {} ;

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 A19, A21, XBOOLE_0:def 4;

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

set h = L2 (#) (H ^ q);

A24: ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) = (Carrier L1) \/ ((Carrier (L1 + L2)) \/ (Carrier L2)) by XBOOLE_1:4;

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

then A25: rng (G ^ p) = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) by A24, XBOOLE_1:7, XBOOLE_1:12;

A26: len q = len (L2 (#) q) by RLVECT_2:def 7;

now :: thesis: for k being Nat st k in dom q holds

(L2 (#) q) . k = 0 * (q /. k)

then A29: Sum (L2 (#) q) =
0 * (Sum q)
by A26, RLVECT_2:3
(L2 (#) q) . k = 0 * (q /. k)

let k be Nat; :: thesis: ( k in dom q implies (L2 (#) q) . k = 0 * (q /. k) )

assume A27: k in dom q ; :: thesis: (L2 (#) q) . k = 0 * (q /. k)

then q /. k = q . k by PARTFUN1:def 6;

then q /. k in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2) by A21, A27, FUNCT_1:def 3;

then A28: not q /. k in Carrier L2 by XBOOLE_0:def 5;

k in dom (L2 (#) q) by A26, A27, FINSEQ_3:29;

then (L2 (#) q) . k = (L2 . (q /. k)) * (q /. k) by RLVECT_2:def 7;

hence (L2 (#) q) . k = 0 * (q /. k) by A28; :: thesis: verum

end;assume A27: k in dom q ; :: thesis: (L2 (#) q) . k = 0 * (q /. k)

then q /. k = q . k by PARTFUN1:def 6;

then q /. k in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2) by A21, A27, FUNCT_1:def 3;

then A28: not q /. k in Carrier L2 by XBOOLE_0:def 5;

k in dom (L2 (#) q) by A26, A27, FINSEQ_3:29;

then (L2 (#) q) . k = (L2 . (q /. k)) * (q /. k) by RLVECT_2:def 7;

hence (L2 (#) q) . k = 0 * (q /. k) by A28; :: thesis: verum

.= 0. V by RLVECT_1:10 ;

A30: Sum (L2 (#) (H ^ q)) = Sum ((L2 (#) H) ^ (L2 (#) q)) by Lm1

.= (Sum (L2 (#) H)) + (0. V) by A29, RLVECT_1:41

.= Sum (L2 (#) H) ;

deffunc H

set g = L1 (#) (G ^ p);

consider P being FinSequence such that

A31: len P = len (F ^ r) and

A32: for k being Nat st k in dom P holds

P . k = H

A33: dom P = Seg (len (F ^ r)) by A31, FINSEQ_1:def 3;

A34: len p = len (L1 (#) p) by RLVECT_2:def 7;

now :: thesis: for k being Nat st k in dom p holds

(L1 (#) p) . k = 0 * (p /. k)

then A37: Sum (L1 (#) p) =
0 * (Sum p)
by A34, RLVECT_2:3
(L1 (#) p) . k = 0 * (p /. k)

let k be Nat; :: thesis: ( k in dom p implies (L1 (#) p) . k = 0 * (p /. k) )

assume A35: k in dom p ; :: thesis: (L1 (#) p) . k = 0 * (p /. k)

then p /. k = p . k by PARTFUN1:def 6;

then p /. k in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L1) by A15, A35, FUNCT_1:def 3;

then A36: not p /. k in Carrier L1 by XBOOLE_0:def 5;

k in dom (L1 (#) p) by A34, A35, FINSEQ_3:29;

then (L1 (#) p) . k = (L1 . (p /. k)) * (p /. k) by RLVECT_2:def 7;

hence (L1 (#) p) . k = 0 * (p /. k) by A36; :: thesis: verum

end;assume A35: k in dom p ; :: thesis: (L1 (#) p) . k = 0 * (p /. k)

then p /. k = p . k by PARTFUN1:def 6;

then p /. k in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L1) by A15, A35, FUNCT_1:def 3;

then A36: not p /. k in Carrier L1 by XBOOLE_0:def 5;

k in dom (L1 (#) p) by A34, A35, FINSEQ_3:29;

then (L1 (#) p) . k = (L1 . (p /. k)) * (p /. k) by RLVECT_2:def 7;

hence (L1 (#) p) . k = 0 * (p /. k) by A36; :: thesis: verum

.= 0. V by RLVECT_1:10 ;

A38: Sum (L1 (#) (G ^ p)) = Sum ((L1 (#) G) ^ (L1 (#) p)) by Lm1

.= (Sum (L1 (#) G)) + (0. V) by A37, RLVECT_1:41

.= Sum (L1 (#) G) ;

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

then A39: rng (F ^ r) = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) by A6, XBOOLE_1:7, XBOOLE_1:12;

rng G misses rng p

proof

then A40:
G ^ p is one-to-one
by A12, A16, FINSEQ_3:91;
set x = the Element of (rng G) /\ (rng p);

assume not rng G misses rng p ; :: thesis: contradiction

then (rng G) /\ (rng p) <> {} ;

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, A15, XBOOLE_0:def 4;

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

end;assume not rng G misses rng p ; :: thesis: contradiction

then (rng G) /\ (rng p) <> {} ;

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, A15, XBOOLE_0:def 4;

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

then A41: len (G ^ p) = len (F ^ r) by A7, A25, A39, FINSEQ_1:48;

A42: dom P = Seg (len (F ^ r)) by A31, FINSEQ_1:def 3;

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

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

A46:
rng P c= Seg (len (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 A44: x in dom (G ^ p) ; :: thesis: (G ^ p) . x = (F ^ r) . (P . x)

then reconsider n = x as Element of NAT by FINSEQ_3:23;

(G ^ p) . n in rng (F ^ r) by A25, A39, A44, FUNCT_1:def 3;

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

n in Seg (len (F ^ r)) by A41, A44, FINSEQ_1:def 3;

then (F ^ r) . (P . n) = (F ^ r) . ((F ^ r) <- ((G ^ p) . n)) by A32, A42

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

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

end;assume A44: x in dom (G ^ p) ; :: thesis: (G ^ p) . x = (F ^ r) . (P . x)

then reconsider n = x as Element of NAT by FINSEQ_3:23;

(G ^ p) . n in rng (F ^ r) by A25, A39, A44, FUNCT_1:def 3;

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

n in Seg (len (F ^ r)) by A41, A44, FINSEQ_1:def 3;

then (F ^ r) . (P . n) = (F ^ r) . ((F ^ r) <- ((G ^ p) . n)) by A32, A42

.= (G ^ p) . n by A45, 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 Seg (len (F ^ r)) )

assume x in rng P ; :: thesis: x in Seg (len (F ^ r))

then consider y being object such that

A47: y in dom P and

A48: P . y = x by FUNCT_1:def 3;

reconsider y = y as Element of NAT by A47, FINSEQ_3:23;

y in Seg (len (F ^ r)) by A31, A47, FINSEQ_1:def 3;

then y in dom (G ^ p) by A41, FINSEQ_1:def 3;

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

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

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

then P . y in dom (F ^ r) by A49, FINSEQ_4:def 3;

hence x in Seg (len (F ^ r)) by A48, FINSEQ_1:def 3; :: thesis: verum

end;assume x in rng P ; :: thesis: x in Seg (len (F ^ r))

then consider y being object such that

A47: y in dom P and

A48: P . y = x by FUNCT_1:def 3;

reconsider y = y as Element of NAT by A47, FINSEQ_3:23;

y in Seg (len (F ^ r)) by A31, A47, FINSEQ_1:def 3;

then y in dom (G ^ p) by A41, FINSEQ_1:def 3;

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

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

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

then P . y in dom (F ^ r) by A49, FINSEQ_4:def 3;

hence x in Seg (len (F ^ r)) by A48, FINSEQ_1: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 A51:
G ^ p = (F ^ r) * P
by A43, 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) )

A50: x in dom P and

P . x in dom (F ^ r) ; :: thesis: x in dom (G ^ p)

x in Seg (len P) by A50, FINSEQ_1:def 3;

hence x in dom (G ^ p) by A41, A31, FINSEQ_1:def 3; :: 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 that
assume
x in dom (G ^ p)
; :: thesis: ( x in dom P & P . x in dom (F ^ r) )

then x in Seg (len P) by A41, A31, FINSEQ_1:def 3;

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;

then P . x in Seg (len (F ^ r)) by A46;

hence P . x in dom (F ^ r) by FINSEQ_1:def 3; :: thesis: verum

end;then x in Seg (len P) by A41, A31, FINSEQ_1:def 3;

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;

then P . x in Seg (len (F ^ r)) by A46;

hence P . x in dom (F ^ r) by FINSEQ_1:def 3; :: thesis: verum

A50: x in dom P and

P . x in dom (F ^ r) ; :: thesis: x in dom (G ^ p)

x in Seg (len P) by A50, FINSEQ_1:def 3;

hence x in dom (G ^ p) by A41, A31, FINSEQ_1:def 3; :: thesis: verum

Seg (len (F ^ r)) c= rng P

proof

then A55:
Seg (len (F ^ r)) = rng P
by A46;
set f = ((F ^ r) ") * (G ^ p);

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Seg (len (F ^ r)) or x in rng P )

assume A52: x in Seg (len (F ^ r)) ; :: thesis: x in rng P

dom ((F ^ r) ") = rng (G ^ p) by A7, A25, A39, FUNCT_1:33;

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

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

A54: rng P c= dom (F ^ r) by A46, FINSEQ_1:def 3;

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

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

.= P by A54, RELAT_1:53 ;

hence x in rng P by A52, A53, FINSEQ_1:def 3; :: thesis: verum

end;let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Seg (len (F ^ r)) or x in rng P )

assume A52: x in Seg (len (F ^ r)) ; :: thesis: x in rng P

dom ((F ^ r) ") = rng (G ^ p) by A7, A25, A39, FUNCT_1:33;

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

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

A54: rng P c= dom (F ^ r) by A46, FINSEQ_1:def 3;

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

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

.= P by A54, RELAT_1:53 ;

hence x in rng P by A52, A53, FINSEQ_1:def 3; :: thesis: verum

then A56: P is one-to-one by A33, FINSEQ_4:60;

reconsider P = P as Function of (Seg (len (F ^ r))),(Seg (len (F ^ r))) by A46, A33, FUNCT_2:2;

reconsider P = P as Permutation of (Seg (len (F ^ r))) by A55, A56, FUNCT_2:57;

A57: len ((L1 + L2) (#) (F ^ r)) = len (F ^ r) by RLVECT_2:def 7;

then A58: Seg (len (F ^ r)) = dom ((L1 + L2) (#) (F ^ r)) by FINSEQ_1:def 3;

then reconsider Fp = ((L1 + L2) (#) (F ^ r)) * P as FinSequence of the carrier of V by FINSEQ_2:47;

A59: len (L1 (#) (G ^ p)) = len (G ^ p) by RLVECT_2:def 7;

deffunc H

consider R being FinSequence such that

A60: len R = len (H ^ q) and

A61: for k being Nat st k in dom R holds

R . k = H

A62: dom R = Seg (len (H ^ q)) by A60, FINSEQ_1:def 3;

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 A19, A21, XBOOLE_1:39;

then A63: rng (H ^ q) = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) by XBOOLE_1:7, XBOOLE_1:12;

then A64: len (G ^ p) = len (H ^ q) by A23, A40, A25, FINSEQ_1:48;

A65: dom R = Seg (len (H ^ q)) by A60, FINSEQ_1:def 3;

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

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

A69:
rng R c= Seg (len (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 A67: x in dom (G ^ p) ; :: thesis: (G ^ p) . x = (H ^ q) . (R . x)

then reconsider n = x as Element of NAT by FINSEQ_3:23;

(G ^ p) . n in rng (H ^ q) by A25, A63, A67, FUNCT_1:def 3;

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

n in Seg (len (H ^ q)) by A64, A67, FINSEQ_1:def 3;

then (H ^ q) . (R . n) = (H ^ q) . ((H ^ q) <- ((G ^ p) . n)) by A61, A65

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

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

end;assume A67: x in dom (G ^ p) ; :: thesis: (G ^ p) . x = (H ^ q) . (R . x)

then reconsider n = x as Element of NAT by FINSEQ_3:23;

(G ^ p) . n in rng (H ^ q) by A25, A63, A67, FUNCT_1:def 3;

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

n in Seg (len (H ^ q)) by A64, A67, FINSEQ_1:def 3;

then (H ^ q) . (R . n) = (H ^ q) . ((H ^ q) <- ((G ^ p) . n)) by A61, A65

.= (G ^ p) . n by A68, 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 Seg (len (H ^ q)) )

assume x in rng R ; :: thesis: x in Seg (len (H ^ q))

then consider y being object such that

A70: y in dom R and

A71: R . y = x by FUNCT_1:def 3;

reconsider y = y as Element of NAT by A70, FINSEQ_3:23;

y in Seg (len (H ^ q)) by A60, A70, FINSEQ_1:def 3;

then y in dom (G ^ p) by A64, FINSEQ_1:def 3;

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

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

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

then R . y in dom (H ^ q) by A72, FINSEQ_4:def 3;

hence x in Seg (len (H ^ q)) by A71, FINSEQ_1:def 3; :: thesis: verum

end;assume x in rng R ; :: thesis: x in Seg (len (H ^ q))

then consider y being object such that

A70: y in dom R and

A71: R . y = x by FUNCT_1:def 3;

reconsider y = y as Element of NAT by A70, FINSEQ_3:23;

y in Seg (len (H ^ q)) by A60, A70, FINSEQ_1:def 3;

then y in dom (G ^ p) by A64, FINSEQ_1:def 3;

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

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

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

then R . y in dom (H ^ q) by A72, FINSEQ_4:def 3;

hence x in Seg (len (H ^ q)) by A71, FINSEQ_1: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 A74:
G ^ p = (H ^ q) * R
by A66, 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) )

A73: x in dom R and

R . x in dom (H ^ q) ; :: thesis: x in dom (G ^ p)

x in Seg (len R) by A73, FINSEQ_1:def 3;

hence x in dom (G ^ p) by A64, A60, FINSEQ_1:def 3; :: 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 that
assume
x in dom (G ^ p)
; :: thesis: ( x in dom R & R . x in dom (H ^ q) )

then x in Seg (len R) by A64, A60, FINSEQ_1:def 3;

hence x in dom R by FINSEQ_1:def 3; :: thesis: R . x in dom (H ^ q)

then R . x in rng R by FUNCT_1:def 3;

then R . x in Seg (len (H ^ q)) by A69;

hence R . x in dom (H ^ q) by FINSEQ_1:def 3; :: thesis: verum

end;then x in Seg (len R) by A64, A60, FINSEQ_1:def 3;

hence x in dom R by FINSEQ_1:def 3; :: thesis: R . x in dom (H ^ q)

then R . x in rng R by FUNCT_1:def 3;

then R . x in Seg (len (H ^ q)) by A69;

hence R . x in dom (H ^ q) by FINSEQ_1:def 3; :: thesis: verum

A73: x in dom R and

R . x in dom (H ^ q) ; :: thesis: x in dom (G ^ p)

x in Seg (len R) by A73, FINSEQ_1:def 3;

hence x in dom (G ^ p) by A64, A60, FINSEQ_1:def 3; :: thesis: verum

Seg (len (H ^ q)) c= rng R

proof

then A78:
Seg (len (H ^ q)) = rng R
by A69;
set f = ((H ^ q) ") * (G ^ p);

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Seg (len (H ^ q)) or x in rng R )

assume A75: x in Seg (len (H ^ q)) ; :: thesis: x in rng R

dom ((H ^ q) ") = rng (G ^ p) by A23, A25, A63, FUNCT_1:33;

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

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

A77: rng R c= dom (H ^ q) by A69, FINSEQ_1:def 3;

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

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

.= R by A77, RELAT_1:53 ;

hence x in rng R by A75, A76, FINSEQ_1:def 3; :: thesis: verum

end;let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Seg (len (H ^ q)) or x in rng R )

assume A75: x in Seg (len (H ^ q)) ; :: thesis: x in rng R

dom ((H ^ q) ") = rng (G ^ p) by A23, A25, A63, FUNCT_1:33;

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

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

A77: rng R c= dom (H ^ q) by A69, FINSEQ_1:def 3;

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

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

.= R by A77, RELAT_1:53 ;

hence x in rng R by A75, A76, FINSEQ_1:def 3; :: thesis: verum

then A79: R is one-to-one by A62, FINSEQ_4:60;

reconsider R = R as Function of (Seg (len (H ^ q))),(Seg (len (H ^ q))) by A69, A62, FUNCT_2:2;

reconsider R = R as Permutation of (Seg (len (H ^ q))) by A78, A79, FUNCT_2:57;

A80: len (L2 (#) (H ^ q)) = len (H ^ q) by RLVECT_2:def 7;

then A81: Seg (len (H ^ q)) = dom (L2 (#) (H ^ q)) by FINSEQ_1:def 3;

then reconsider Hp = (L2 (#) (H ^ q)) * R as FinSequence of the carrier of V by FINSEQ_2:47;

A82: len Hp = len (G ^ p) by A64, A80, A81, FINSEQ_2:44;

deffunc H

consider I being FinSequence such that

A83: len I = len (G ^ p) and

A84: for k being Nat st k in dom I holds

I . k = H

dom I = Seg (len (G ^ p)) by A83, FINSEQ_1:def 3;

then A85: for k being Nat st k in Seg (len (G ^ p)) holds

I . k = H

rng I c= the carrier of V

proof

then reconsider I = I as FinSequence of the carrier of V 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 V )

assume x in rng I ; :: thesis: x in the carrier of V

then consider y being object such that

A86: y in dom I and

A87: I . y = x by FUNCT_1:def 3;

reconsider y = y as Element of NAT by A86, FINSEQ_3:23;

I . y = ((L1 (#) (G ^ p)) /. y) + (Hp /. y) by A84, A86;

hence x in the carrier of V by A87; :: thesis: verum

end;assume x in rng I ; :: thesis: x in the carrier of V

then consider y being object such that

A86: y in dom I and

A87: I . y = x by FUNCT_1:def 3;

reconsider y = y as Element of NAT by A86, FINSEQ_3:23;

I . y = ((L1 (#) (G ^ p)) /. y) + (Hp /. y) by A84, A86;

hence x in the carrier of V by A87; :: thesis: verum

A88: len Fp = len I by A41, A57, A58, A83, FINSEQ_2:44;

A89: now :: thesis: for x being object st x in dom I holds

I . x = Fp . x

dom (L2 (#) (H ^ q)) = Seg (len (L2 (#) (H ^ q)))
by FINSEQ_1:def 3;I . x = Fp . x

let x be object ; :: thesis: ( x in dom I implies I . x = Fp . x )

assume A90: x in dom I ; :: thesis: I . x = Fp . x

then reconsider k = x as Element of NAT by FINSEQ_3:23;

A91: x in dom Hp by A83, A82, A90, FINSEQ_3:29;

k in dom R by A64, A62, A83, A90, FINSEQ_1:def 3;

then A92: R . k in dom R by A78, A62, FUNCT_1:def 3;

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

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

A93: R . k in dom (H ^ q) by A60, A92, FINSEQ_3:29;

A94: x in dom (G ^ p) by A83, A90, FINSEQ_3:29;

then (H ^ q) . j = (G ^ p) . k by A66

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

then A95: (L2 (#) (H ^ q)) . j = (L2 . ((G ^ p) /. k)) * ((G ^ p) /. k) by A93, RLVECT_2:24;

k in dom P by A41, A33, A83, A90, FINSEQ_1:def 3;

then A96: P . k in dom P by A55, A33, FUNCT_1:def 3;

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

A97: P . k in dom (F ^ r) by A31, A96, FINSEQ_3:29;

x in dom Fp by A88, A90, FINSEQ_3:29;

then A98: Fp . k = ((L1 + L2) (#) (F ^ r)) . (P . k) by FUNCT_1:12;

k in dom Hp by A83, A82, A90, FINSEQ_3:29;

then A99: Hp /. k = ((L2 (#) (H ^ q)) * R) . k by PARTFUN1:def 6

.= (L2 (#) (H ^ q)) . (R . k) by A91, FUNCT_1:12 ;

A100: x in dom (L1 (#) (G ^ p)) by A83, A59, A90, FINSEQ_3:29;

(F ^ r) . l = (G ^ p) . k by A43, A94

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

then A101: ((L1 + L2) (#) (F ^ r)) . l = ((L1 + L2) . ((G ^ p) /. k)) * ((G ^ p) /. k) by A97, RLVECT_2:24

.= ((L1 . ((G ^ p) /. k)) + (L2 . ((G ^ p) /. k))) * ((G ^ p) /. k) by RLVECT_2:def 10

.= ((L1 . ((G ^ p) /. k)) * ((G ^ p) /. k)) + ((L2 . ((G ^ p) /. k)) * ((G ^ p) /. k)) by RLVECT_1:def 6 ;

k in dom (L1 (#) (G ^ p)) by A83, A59, A90, FINSEQ_3:29;

then (L1 (#) (G ^ p)) /. k = (L1 (#) (G ^ p)) . k by PARTFUN1:def 6

.= (L1 . ((G ^ p) /. k)) * ((G ^ p) /. k) by A100, RLVECT_2:def 7 ;

hence I . x = Fp . x by A84, A90, A99, A95, A98, A101; :: thesis: verum

end;assume A90: x in dom I ; :: thesis: I . x = Fp . x

then reconsider k = x as Element of NAT by FINSEQ_3:23;

A91: x in dom Hp by A83, A82, A90, FINSEQ_3:29;

k in dom R by A64, A62, A83, A90, FINSEQ_1:def 3;

then A92: R . k in dom R by A78, A62, FUNCT_1:def 3;

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

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

A93: R . k in dom (H ^ q) by A60, A92, FINSEQ_3:29;

A94: x in dom (G ^ p) by A83, A90, FINSEQ_3:29;

then (H ^ q) . j = (G ^ p) . k by A66

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

then A95: (L2 (#) (H ^ q)) . j = (L2 . ((G ^ p) /. k)) * ((G ^ p) /. k) by A93, RLVECT_2:24;

k in dom P by A41, A33, A83, A90, FINSEQ_1:def 3;

then A96: P . k in dom P by A55, A33, FUNCT_1:def 3;

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

A97: P . k in dom (F ^ r) by A31, A96, FINSEQ_3:29;

x in dom Fp by A88, A90, FINSEQ_3:29;

then A98: Fp . k = ((L1 + L2) (#) (F ^ r)) . (P . k) by FUNCT_1:12;

k in dom Hp by A83, A82, A90, FINSEQ_3:29;

then A99: Hp /. k = ((L2 (#) (H ^ q)) * R) . k by PARTFUN1:def 6

.= (L2 (#) (H ^ q)) . (R . k) by A91, FUNCT_1:12 ;

A100: x in dom (L1 (#) (G ^ p)) by A83, A59, A90, FINSEQ_3:29;

(F ^ r) . l = (G ^ p) . k by A43, A94

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

then A101: ((L1 + L2) (#) (F ^ r)) . l = ((L1 + L2) . ((G ^ p) /. k)) * ((G ^ p) /. k) by A97, RLVECT_2:24

.= ((L1 . ((G ^ p) /. k)) + (L2 . ((G ^ p) /. k))) * ((G ^ p) /. k) by RLVECT_2:def 10

.= ((L1 . ((G ^ p) /. k)) * ((G ^ p) /. k)) + ((L2 . ((G ^ p) /. k)) * ((G ^ p) /. k)) by RLVECT_1:def 6 ;

k in dom (L1 (#) (G ^ p)) by A83, A59, A90, FINSEQ_3:29;

then (L1 (#) (G ^ p)) /. k = (L1 (#) (G ^ p)) . k by PARTFUN1:def 6

.= (L1 . ((G ^ p) /. k)) * ((G ^ p) /. k) by A100, RLVECT_2:def 7 ;

hence I . x = Fp . x by A84, A90, A99, A95, A98, A101; :: thesis: verum

then A102: Sum Hp = Sum (L2 (#) (H ^ q)) by A80, RLVECT_2:7;

dom ((L1 + L2) (#) (F ^ r)) = Seg (len ((L1 + L2) (#) (F ^ r))) by FINSEQ_1:def 3;

then A103: Sum Fp = Sum ((L1 + L2) (#) (F ^ r)) by A57, RLVECT_2:7;

( dom I = Seg (len I) & dom Fp = Seg (len I) ) by A88, FINSEQ_1:def 3;

then A104: I = Fp by A89, FUNCT_1:2;

Seg (len (G ^ p)) = dom (L1 (#) (G ^ p)) by A59, FINSEQ_1:def 3;

hence Sum (L1 + L2) = (Sum L1) + (Sum L2) by A3, A14, A20, A38, A30, A17, A103, A102, A83, A85, A82, A59, A104, RLVECT_2:2; :: thesis: verum