let s be XFinSequence; for p, q being XFinSequence-yielding FinSequence holds
( s ^+ (p ^ q) = (s ^+ p) ^ (s ^+ q) & (p ^ q) +^ s = (p +^ s) ^ (q +^ s) )
let p, q be XFinSequence-yielding FinSequence; ( s ^+ (p ^ q) = (s ^+ p) ^ (s ^+ q) & (p ^ q) +^ s = (p +^ s) ^ (q +^ s) )
A1:
now for k being Nat st k in dom (s ^+ (p ^ q)) holds
(s ^+ (p ^ q)) . k = ((s ^+ p) ^ (s ^+ q)) . klet k be
Nat;
( k in dom (s ^+ (p ^ q)) implies (s ^+ (p ^ q)) . k = ((s ^+ p) ^ (s ^+ q)) . k )assume A2:
k in dom (s ^+ (p ^ q))
;
(s ^+ (p ^ q)) . k = ((s ^+ p) ^ (s ^+ q)) . kthen A3:
k in dom (p ^ q)
by Def2;
now (s ^+ (p ^ q)) . k = ((s ^+ p) ^ (s ^+ q)) . kper cases
( k in dom p or not k in dom p )
;
suppose A6:
not
k in dom p
;
(s ^+ (p ^ q)) . k = ((s ^+ p) ^ (s ^+ q)) . kA7:
k <= len (p ^ q)
by A3, FINSEQ_3:25;
(
k < 1 or
k > len p )
by A6, FINSEQ_3:25;
then consider i being
Nat such that A8:
k = (len p) + i
and A9:
(
i >= 1 &
i <= len q )
by A2, A7, Th2, FINSEQ_3:25;
A10:
i in dom q
by A9, FINSEQ_3:25;
then A11:
i in dom (s ^+ q)
by Def2;
A12:
len (s ^+ p) = len p
by Th5;
thus (s ^+ (p ^ q)) . k =
s ^ ((p ^ q) . ((len p) + i))
by A3, A8, Def2
.=
s ^ (q . i)
by A10, FINSEQ_1:def 7
.=
(s ^+ q) . i
by A10, Def2
.=
((s ^+ p) ^ (s ^+ q)) . k
by A8, A11, A12, FINSEQ_1:def 7
;
verum end; end; end; hence
(s ^+ (p ^ q)) . k = ((s ^+ p) ^ (s ^+ q)) . k
;
verum end;
len (s ^+ (p ^ q)) =
len (p ^ q)
by Th5
.=
(len p) + (len q)
by FINSEQ_1:22
.=
(len (s ^+ p)) + (len q)
by Th5
.=
(len (s ^+ p)) + (len (s ^+ q))
by Th5
.=
len ((s ^+ p) ^ (s ^+ q))
by FINSEQ_1:22
;
then
dom (s ^+ (p ^ q)) = dom ((s ^+ p) ^ (s ^+ q))
by FINSEQ_3:29;
hence
s ^+ (p ^ q) = (s ^+ p) ^ (s ^+ q)
by A1, FINSEQ_1:13; (p ^ q) +^ s = (p +^ s) ^ (q +^ s)
A13:
now for k being Nat st k in dom ((p ^ q) +^ s) holds
((p ^ q) +^ s) . k = ((p +^ s) ^ (q +^ s)) . klet k be
Nat;
( k in dom ((p ^ q) +^ s) implies ((p ^ q) +^ s) . k = ((p +^ s) ^ (q +^ s)) . k )assume A14:
k in dom ((p ^ q) +^ s)
;
((p ^ q) +^ s) . k = ((p +^ s) ^ (q +^ s)) . kthen A15:
k in dom (p ^ q)
by Def3;
now ((p ^ q) +^ s) . k = ((p +^ s) ^ (q +^ s)) . kper cases
( k in dom p or not k in dom p )
;
suppose A18:
not
k in dom p
;
((p ^ q) +^ s) . k = ((p +^ s) ^ (q +^ s)) . kA19:
k <= len (p ^ q)
by A15, FINSEQ_3:25;
(
k < 1 or
k > len p )
by A18, FINSEQ_3:25;
then consider i being
Nat such that A20:
k = (len p) + i
and A21:
(
i >= 1 &
i <= len q )
by A14, A19, Th2, FINSEQ_3:25;
A22:
i in dom q
by A21, FINSEQ_3:25;
then A23:
i in dom (q +^ s)
by Def3;
A24:
len (p +^ s) = len p
by Th5;
thus ((p ^ q) +^ s) . k =
((p ^ q) . ((len p) + i)) ^ s
by A15, A20, Def3
.=
(q . i) ^ s
by A22, FINSEQ_1:def 7
.=
(q +^ s) . i
by A22, Def3
.=
((p +^ s) ^ (q +^ s)) . k
by A20, A23, A24, FINSEQ_1:def 7
;
verum end; end; end; hence
((p ^ q) +^ s) . k = ((p +^ s) ^ (q +^ s)) . k
;
verum end;
len ((p ^ q) +^ s) =
len (p ^ q)
by Th5
.=
(len p) + (len q)
by FINSEQ_1:22
.=
(len (p +^ s)) + (len q)
by Th5
.=
(len (p +^ s)) + (len (q +^ s))
by Th5
.=
len ((p +^ s) ^ (q +^ s))
by FINSEQ_1:22
;
then
dom ((p ^ q) +^ s) = dom ((p +^ s) ^ (q +^ s))
by FINSEQ_3:29;
hence
(p ^ q) +^ s = (p +^ s) ^ (q +^ s)
by A13, FINSEQ_1:13; verum