let R be Ring; :: thesis:
let V be RightMod of R; :: thesis:
let L1, L2 be Linear_Combination of V; :: thesis:
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 V 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 V 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 V by A7, FINSEQ_1:def 4;
consider F being FinSequence of V such that
A9: F is one-to-one and
A10: rng F = Carrier (L1 + L2) and
A11: Sum ((L1 + L2) (#) F) = Sum (L1 + L2) by Def7;
set FF = F ^ r;
consider G being FinSequence of V such that
A12: G is one-to-one and
A13: rng G = Carrier L1 and
A14: Sum (L1 (#) G) = Sum L1 by Def7;
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

set x = the Element of (rng F) /\ (rng r);
assume not rng F misses rng r ; :: thesis:
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 A10, A4, XBOOLE_0:def 4;
hence contradiction by XBOOLE_0:def 5; :: thesis:

end;

then A17: F ^ r is one-to-one by A9, A5, FINSEQ_3:91;
rng G misses rng p

proof

set x = the Element of (rng G) /\ (rng p);
assume not rng G misses rng p ; :: thesis:
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, A1, XBOOLE_0:def 4;
hence contradiction by XBOOLE_0:def 5; :: thesis:

end;

then A18: G ^ p is one-to-one by A12, A2, FINSEQ_3:91;
then A19: len (G ^ p) = len (F ^ r) by A17, A16, A15, FINSEQ_1:48;
deffunc H₁( 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₁(k) from FINSEQ_1:sch 2();
A22: dom P = Seg (len (F ^ r)) by A20, FINSEQ_1:def 3;

A23: now :: thesis:

let x be object ; :: thesis:
assume A24: x in dom (G ^ p) ; :: thesis:
then reconsider n = x as Nat by FINSEQ_3:23;
(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;
n in Seg (len (F ^ r)) by A19, A24, FINSEQ_1:def 3;
then (F ^ r) . (P . n) = (F ^ r) . ((F ^ r) <- ((G ^ p) . n)) by A21, A22
.= (G ^ p) . n by A25, FINSEQ_4:def 3 ;
hence (G ^ p) . x = (F ^ r) . (P . x) ; :: thesis:

end;

A26: dom (G ^ p) = dom (F ^ r) by A19, FINSEQ_3:29;
A27: rng P c= dom (F ^ r)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng P ; :: thesis:
then consider y being object such that
A28: y in dom P and
A29: P . y = x by FUNCT_1:def 3;
reconsider y = y as Nat by A28, FINSEQ_3:23;
y in dom (F ^ r) by A20, A28, FINSEQ_3:29;
then (G ^ p) . y in rng (F ^ r) by A16, A15, A26, FUNCT_1:def 3;
then A30: F ^ r just_once_values (G ^ p) . y by A17, FINSEQ_4:8;
P . y = (F ^ r) <- ((G ^ p) . y) by A21, A28;
hence x in dom (F ^ r) by A29, A30, FINSEQ_4:def 3; :: thesis:

end;

now :: thesis:

let x be object ; :: thesis:
thus ( x in dom (G ^ p) implies ( x in dom P & P . x in dom (F ^ r) ) ) :: thesis:

proof

assume x in dom (G ^ p) ; :: thesis:
hence x in dom P by A19, A20, FINSEQ_3:29; :: thesis:
then P . x in rng P by FUNCT_1:def 3;
hence P . x in dom (F ^ r) by A27; :: thesis:

end;

assume that
A31: x in dom P and
P . x in dom (F ^ r) ; :: thesis:
x in Seg (len P) by A31, FINSEQ_1:def 3;
hence x in dom (G ^ p) by A19, A20, FINSEQ_1:def 3; :: thesis:

end;

then A32: G ^ p = (F ^ r) * P by A23, FUNCT_1:10;
dom (F ^ r) c= rng P

proof

set f = ((F ^ r) ") * (G ^ p);
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A33: x in dom (F ^ r) ; :: thesis:
dom ((F ^ r) ") = rng (G ^ p) by A17, A16, A15, FUNCT_1:33;
then A34: 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 A32, RELAT_1:36
.= (id (dom (F ^ r))) * P by A17, FUNCT_1:39
.= P by A27, RELAT_1:53 ;
hence x in rng P by A33, A34; :: thesis:

end;

then A35: dom (F ^ r) = rng P by A27;
A36: len r = len ((L1 + L2) (#) r) by Def6;

now :: thesis:

let k be Nat; :: thesis:
assume A37: k in dom r ; :: thesis:
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, A37, FUNCT_1:def 3;
then A38: not r /. k in Carrier (L1 + L2) by XBOOLE_0:def 5;
k in dom ((L1 + L2) (#) r) by A36, A37, FINSEQ_3:29;
then ((L1 + L2) (#) r) . k = (r /. k) * ((L1 + L2) . (r /. k)) by Def6;
hence ((L1 + L2) (#) r) . k = (r /. k) * (0. R) by A38; :: thesis:

end;

then A39: Sum ((L1 + L2) (#) r) = (Sum r) * (0. R) by A36, Lm2
.= 0. V by VECTSP_2:32 ;
A40: len p = len (L1 (#) p) by Def6;

now :: thesis:

let k be Nat; :: thesis:
assume A41: k in dom p ; :: thesis:
then p /. k = p . k by PARTFUN1:def 6;
then p /. k in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L1) by A1, A41, FUNCT_1:def 3;
then A42: not p /. k in Carrier L1 by XBOOLE_0:def 5;
k in dom (L1 (#) p) by A40, A41, FINSEQ_3:29;
then (L1 (#) p) . k = (p /. k) * (L1 . (p /. k)) by Def6;
hence (L1 (#) p) . k = (p /. k) * (0. R) by A42; :: thesis:

end;

then A43: Sum (L1 (#) p) = (Sum p) * (0. R) by A40, Lm2
.= 0. V by VECTSP_2:32 ;
set f = (L1 + L2) (#) (F ^ r);
consider H being FinSequence of V such that
A44: H is one-to-one and
A45: rng H = Carrier L2 and
A46: Sum (L2 (#) H) = Sum L2 by Def7;
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:
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 A45, A7, XBOOLE_0:def 4;
hence contradiction by XBOOLE_0:def 5; :: thesis:

end;

then A47: H ^ q is one-to-one by A44, A8, FINSEQ_3:91;
A48: len q = len (L2 (#) q) by Def6;

now :: thesis:

let k be Nat; :: thesis:
assume A49: k in dom q ; :: thesis:
then q /. k = q . k by PARTFUN1:def 6;
then q /. k in (((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2)) \ (Carrier L2) by A7, A49, FUNCT_1:def 3;
then A50: not q /. k in Carrier L2 by XBOOLE_0:def 5;
k in dom (L2 (#) q) by A48, A49, FINSEQ_3:29;
then (L2 (#) q) . k = (q /. k) * (L2 . (q /. k)) by Def6;
hence (L2 (#) q) . k = (q /. k) * (0. R) by A50; :: thesis:

end;

then A51: Sum (L2 (#) q) = (Sum q) * (0. R) by A48, Lm2
.= 0. V by VECTSP_2:32 ;
set g = L1 (#) (G ^ p);
A52: len (L1 (#) (G ^ p)) = len (G ^ p) by Def6;
then A53: Seg (len (G ^ p)) = dom (L1 (#) (G ^ p)) by 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 A45, A7, XBOOLE_1:39;
then A54: rng (H ^ q) = ((Carrier (L1 + L2)) \/ (Carrier L1)) \/ (Carrier L2) by XBOOLE_1:7, XBOOLE_1:12;
then A55: len (G ^ p) = len (H ^ q) by A47, A18, A16, FINSEQ_1:48;
deffunc H₂( Nat) -> set = (H ^ q) <- ((G ^ p) . $1);
consider R being FinSequence such that
A56: len R = len (H ^ q) and
A57: for k being Nat st k in dom R holds
R . k = H₂(k) from FINSEQ_1:sch 2();
A58: dom R = Seg (len (H ^ q)) by A56, FINSEQ_1:def 3;

A59: now :: thesis:

let x be object ; :: thesis:
assume A60: x in dom (G ^ p) ; :: thesis:
then reconsider n = x as Nat by FINSEQ_3:23;
(G ^ p) . n in rng (H ^ q) by A16, A54, A60, FUNCT_1:def 3;
then A61: H ^ q just_once_values (G ^ p) . n by A47, FINSEQ_4:8;
n in Seg (len (H ^ q)) by A55, A60, FINSEQ_1:def 3;
then (H ^ q) . (R . n) = (H ^ q) . ((H ^ q) <- ((G ^ p) . n)) by A57, A58
.= (G ^ p) . n by A61, FINSEQ_4:def 3 ;
hence (G ^ p) . x = (H ^ q) . (R . x) ; :: thesis:

end;

A62: dom (G ^ p) = dom (H ^ q) by A55, FINSEQ_3:29;
A63: rng R c= dom (H ^ q)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng R ; :: thesis:
then consider y being object such that
A64: y in dom R and
A65: R . y = x by FUNCT_1:def 3;
reconsider y = y as Nat by A64, FINSEQ_3:23;
y in dom (H ^ q) by A56, A64, FINSEQ_3:29;
then (G ^ p) . y in rng (H ^ q) by A16, A54, A62, FUNCT_1:def 3;
then A66: H ^ q just_once_values (G ^ p) . y by A47, FINSEQ_4:8;
R . y = (H ^ q) <- ((G ^ p) . y) by A57, A64;
hence x in dom (H ^ q) by A65, A66, FINSEQ_4:def 3; :: thesis:

end;

now :: thesis:

let x be object ; :: thesis:
thus ( x in dom (G ^ p) implies ( x in dom R & R . x in dom (H ^ q) ) ) :: thesis:

proof

assume x in dom (G ^ p) ; :: thesis:
then x in Seg (len R) by A55, A56, FINSEQ_1:def 3;
hence x in dom R by FINSEQ_1:def 3; :: thesis:
then R . x in rng R by FUNCT_1:def 3;
hence R . x in dom (H ^ q) by A63; :: thesis:

end;

assume that
A67: x in dom R and
R . x in dom (H ^ q) ; :: thesis:
x in Seg (len R) by A67, FINSEQ_1:def 3;
hence x in dom (G ^ p) by A55, A56, FINSEQ_1:def 3; :: thesis:

end;

then A68: G ^ p = (H ^ q) * R by A59, FUNCT_1:10;
dom (H ^ q) c= rng R

proof

set f = ((H ^ q) ") * (G ^ p);
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A69: x in dom (H ^ q) ; :: thesis:
dom ((H ^ q) ") = rng (G ^ p) by A47, A16, A54, FUNCT_1:33;
then A70: rng (((H ^ q) ") * (G ^ p)) = rng ((H ^ q) ") by RELAT_1:28
.= dom (H ^ q) by A47, FUNCT_1:33 ;
((H ^ q) ") * (G ^ p) = (((H ^ q) ") * (H ^ q)) * R by A68, RELAT_1:36
.= (id (dom (H ^ q))) * R by A47, FUNCT_1:39
.= R by A63, RELAT_1:53 ;
hence x in rng R by A69, A70; :: thesis:

end;

then A71: dom (H ^ q) = rng R by A63;
A72: Sum (L1 (#) (G ^ p)) = Sum ((L1 (#) G) ^ (L1 (#) p)) by Th28
.= (Sum (L1 (#) G)) + (0. V) by A43, RLVECT_1:41
.= Sum (L1 (#) G) by RLVECT_1:def 4 ;
set h = L2 (#) (H ^ q);
A73: Sum (L2 (#) (H ^ q)) = Sum ((L2 (#) H) ^ (L2 (#) q)) by Th28
.= (Sum (L2 (#) H)) + (0. V) by A51, RLVECT_1:41
.= Sum (L2 (#) H) by RLVECT_1:def 4 ;
A74: Sum ((L1 + L2) (#) (F ^ r)) = Sum (((L1 + L2) (#) F) ^ ((L1 + L2) (#) r)) by Th28
.= (Sum ((L1 + L2) (#) F)) + (0. V) by A39, RLVECT_1:41
.= Sum ((L1 + L2) (#) F) by RLVECT_1:def 4 ;
A75: dom P = dom (F ^ r) by A20, FINSEQ_3:29;
then A76: P is one-to-one by A35, FINSEQ_4:60;
A77: dom R = dom (H ^ q) by A56, FINSEQ_3:29;
then A78: R is one-to-one by A71, FINSEQ_4:60;
reconsider R = R as Function of (dom (H ^ q)),(dom (H ^ q)) by A63, A77, FUNCT_2:2;
A79: len (L2 (#) (H ^ q)) = len (H ^ q) by Def6;
then A80: dom (L2 (#) (H ^ q)) = dom (H ^ q) by FINSEQ_3:29;
then reconsider R = R as Function of (dom (L2 (#) (H ^ q))),(dom (L2 (#) (H ^ q))) ;
reconsider Hp = (L2 (#) (H ^ q)) * R as FinSequence of V by FINSEQ_2:47;
reconsider R = R as Permutation of (dom (L2 (#) (H ^ q))) by A71, A78, A80, FUNCT_2:57;
A81: Hp = (L2 (#) (H ^ q)) * R ;
then A82: len Hp = len (G ^ p) by A55, A79, FINSEQ_2:44;
reconsider P = P as Function of (dom (F ^ r)),(dom (F ^ r)) by A27, A75, FUNCT_2:2;
A83: len ((L1 + L2) (#) (F ^ r)) = len (F ^ r) by Def6;
then A84: dom ((L1 + L2) (#) (F ^ r)) = dom (F ^ r) by FINSEQ_3:29;
then reconsider P = P as Function of (dom ((L1 + L2) (#) (F ^ r))),(dom ((L1 + L2) (#) (F ^ r))) ;
reconsider Fp = ((L1 + L2) (#) (F ^ r)) * P as FinSequence of V by FINSEQ_2:47;
reconsider P = P as Permutation of (dom ((L1 + L2) (#) (F ^ r))) by A35, A76, A84, FUNCT_2:57;
A85: Fp = ((L1 + L2) (#) (F ^ r)) * P ;
then A86: Sum Fp = Sum ((L1 + L2) (#) (F ^ r)) by RLVECT_2:7;
deffunc H₃( Nat) -> Element of the carrier of V = ((L1 (#) (G ^ p)) /. $1) + (Hp /. $1);
consider I being FinSequence such that
A87: len I = len (G ^ p) and
A88: for k being Nat st k in dom I holds
I . k = H₃(k) from FINSEQ_1:sch 2();
A89: dom I = Seg (len (G ^ p)) by A87, FINSEQ_1:def 3;
then A90: for k being Nat st k in Seg (len (G ^ p)) holds
I . k = H₃(k) by A88;
rng I c= the carrier of V

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng I ; :: thesis:
then consider y being object such that
A91: y in dom I and
A92: I . y = x by FUNCT_1:def 3;
reconsider y = y as Nat by A91, FINSEQ_3:23;
I . y = ((L1 (#) (G ^ p)) /. y) + (Hp /. y) by A88, A91;
hence x in the carrier of V by A92; :: thesis:

end;

then reconsider I = I as FinSequence of V by FINSEQ_1:def 4;
A93: len Fp = len I by A19, A83, A85, A87, FINSEQ_2:44;

A94: now :: thesis:

let x be object ; :: thesis:
assume A95: x in Seg (len I) ; :: thesis:
then reconsider k = x as Element of NAT ;
A96: x in dom (H ^ q) by A55, A87, A95, FINSEQ_1:def 3;
then R . k in dom R by A71, A77, FUNCT_1:def 3;
then reconsider j = R . k as Nat by FINSEQ_3:23;
A97: x in dom (G ^ p) by A87, A95, FINSEQ_1:def 3;
then A98: (H ^ q) . j = (G ^ p) . k by A59
.= (G ^ p) /. k by A97, PARTFUN1:def 6 ;
P . k in dom P by A26, A62, A35, A75, A96, FUNCT_1:def 3;
then reconsider l = P . k as Nat by FINSEQ_3:23;
set v = (G ^ p) /. k;
A99: x in dom Fp by A93, A95, FINSEQ_1:def 3;
A100: (F ^ r) . l = (G ^ p) . k by A23, A97
.= (G ^ p) /. k by A97, PARTFUN1:def 6 ;
P . k in dom (F ^ r) by A26, A62, A35, A75, A96, FUNCT_1:def 3;
then A101: ((L1 + L2) (#) (F ^ r)) . l = ((G ^ p) /. k) * ((L1 + L2) . ((G ^ p) /. k)) by A100, Th23
.= ((G ^ p) /. k) * ((L1 . ((G ^ p) /. k)) + (L2 . ((G ^ p) /. k))) by Def9
.= (((G ^ p) /. k) * (L1 . ((G ^ p) /. k))) + (((G ^ p) /. k) * (L2 . ((G ^ p) /. k))) by VECTSP_2:def 9 ;
A102: x in dom Hp by A87, A82, A95, FINSEQ_1:def 3;
then A103: Hp /. k = ((L2 (#) (H ^ q)) * R) . k by PARTFUN1:def 6
.= (L2 (#) (H ^ q)) . (R . k) by A102, FUNCT_1:12 ;
R . k in dom (H ^ q) by A71, A77, A96, FUNCT_1:def 3;
then A104: (L2 (#) (H ^ q)) . j = ((G ^ p) /. k) * (L2 . ((G ^ p) /. k)) by A98, Th23;
A105: x in dom (L1 (#) (G ^ p)) by A87, A52, A95, FINSEQ_1:def 3;
then (L1 (#) (G ^ p)) /. k = (L1 (#) (G ^ p)) . k by PARTFUN1:def 6
.= ((G ^ p) /. k) * (L1 . ((G ^ p) /. k)) by A105, Def6 ;
hence I . x = (((G ^ p) /. k) * (L1 . ((G ^ p) /. k))) + (((G ^ p) /. k) * (L2 . ((G ^ p) /. k))) by A87, A88, A89, A95, A103, A104
.= Fp . x by A99, A101, FUNCT_1:12 ;
:: thesis:

end;

( dom I = Seg (len I) & dom Fp = Seg (len I) ) by A93, FINSEQ_1:def 3;
then A106: I = Fp by A94;
Sum Hp = Sum (L2 (#) (H ^ q)) by A81, RLVECT_2:7;
hence Sum (L1 + L2) = (Sum L1) + (Sum L2) by A11, A14, A46, A72, A73, A74, A86, A87, A90, A82, A52, A106, A53, RLVECT_2:2; :: thesis: