let s be XFinSequence; :: thesis: 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; :: thesis: ( s ^+ (p ^ q) = (s ^+ p) ^ (s ^+ q) & (p ^ q) +^ s = (p +^ s) ^ (q +^ s) )
A1: now :: thesis: for k being Nat st k in dom (s ^+ (p ^ q)) holds
(s ^+ (p ^ q)) . k = ((s ^+ p) ^ (s ^+ q)) . k
let k be Nat; :: thesis: ( k in dom (s ^+ (p ^ q)) implies (s ^+ (p ^ q)) . k = ((s ^+ p) ^ (s ^+ q)) . k )
assume A2: k in dom (s ^+ (p ^ q)) ; :: thesis: (s ^+ (p ^ q)) . k = ((s ^+ p) ^ (s ^+ q)) . k
then A3: k in dom (p ^ q) by Def2;
now :: thesis: (s ^+ (p ^ q)) . k = ((s ^+ p) ^ (s ^+ q)) . k
per cases ( k in dom p or not k in dom p ) ;
suppose A4: k in dom p ; :: thesis: (s ^+ (p ^ q)) . k = ((s ^+ p) ^ (s ^+ q)) . k
then A5: k in dom (s ^+ p) by Def2;
thus (s ^+ (p ^ q)) . k = s ^ ((p ^ q) . k) by
.= s ^ (p . k) by
.= (s ^+ p) . k by
.= ((s ^+ p) ^ (s ^+ q)) . k by ; :: thesis: verum
end;
suppose A6: not k in dom p ; :: thesis: (s ^+ (p ^ q)) . k = ((s ^+ p) ^ (s ^+ q)) . k
A7: k <= len (p ^ q) by ;
( k < 1 or k > len p ) by ;
then consider i being Nat such that
A8: k = (len p) + i and
A9: ( i >= 1 & i <= len q ) by ;
A10: i in dom q by ;
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
.= (s ^+ q) . i by
.= ((s ^+ p) ^ (s ^+ q)) . k by ; :: thesis: verum
end;
end;
end;
hence (s ^+ (p ^ q)) . k = ((s ^+ p) ^ (s ^+ q)) . k ; :: thesis: 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 ; :: thesis: (p ^ q) +^ s = (p +^ s) ^ (q +^ s)
A13: now :: thesis: for k being Nat st k in dom ((p ^ q) +^ s) holds
((p ^ q) +^ s) . k = ((p +^ s) ^ (q +^ s)) . k
let k be Nat; :: thesis: ( k in dom ((p ^ q) +^ s) implies ((p ^ q) +^ s) . k = ((p +^ s) ^ (q +^ s)) . k )
assume A14: k in dom ((p ^ q) +^ s) ; :: thesis: ((p ^ q) +^ s) . k = ((p +^ s) ^ (q +^ s)) . k
then A15: k in dom (p ^ q) by Def3;
now :: thesis: ((p ^ q) +^ s) . k = ((p +^ s) ^ (q +^ s)) . k
per cases ( k in dom p or not k in dom p ) ;
suppose A16: k in dom p ; :: thesis: ((p ^ q) +^ s) . k = ((p +^ s) ^ (q +^ s)) . k
then A17: k in dom (p +^ s) by Def3;
thus ((p ^ q) +^ s) . k = ((p ^ q) . k) ^ s by
.= (p . k) ^ s by
.= (p +^ s) . k by
.= ((p +^ s) ^ (q +^ s)) . k by ; :: thesis: verum
end;
suppose A18: not k in dom p ; :: thesis: ((p ^ q) +^ s) . k = ((p +^ s) ^ (q +^ s)) . k
A19: k <= len (p ^ q) by ;
( k < 1 or k > len p ) by ;
then consider i being Nat such that
A20: k = (len p) + i and
A21: ( i >= 1 & i <= len q ) by ;
A22: i in dom q by ;
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
.= (q . i) ^ s by
.= (q +^ s) . i by
.= ((p +^ s) ^ (q +^ s)) . k by ; :: thesis: verum
end;
end;
end;
hence ((p ^ q) +^ s) . k = ((p +^ s) ^ (q +^ s)) . k ; :: thesis: 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 ; :: thesis: verum