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) )
len (s ^+ (p ^ q)) = len (p ^ q) by Th5
.= (len p) + (len q) by FINSEQ_1:35
.= (len (s ^+ p)) + (len q) by Th5
.= (len (s ^+ p)) + (len (s ^+ q)) by Th5
.= len ((s ^+ p) ^ (s ^+ q)) by FINSEQ_1:35 ;
then A1: dom (s ^+ (p ^ q)) = dom ((s ^+ p) ^ (s ^+ q)) by FINSEQ_3:31;

now

let k be Nat; :: thesis: ( k in dom (s ^+ (p ^ q)) implies (s ^+ (p ^ q)) . k = ((s ^+ p) ^ (s ^+ q)) . k )
assume k in dom (s ^+ (p ^ q)) ; :: thesis: (s ^+ (p ^ q)) . k = ((s ^+ p) ^ (s ^+ q)) . k
then A2: k in dom (p ^ q) by Def2;

now

per cases ( k in dom p or not k in dom p ) ;

suppose A3: k in dom p ; :: thesis: (s ^+ (p ^ q)) . k = ((s ^+ p) ^ (s ^+ q)) . k

then A4: k in dom (s ^+ p) by Def2;
thus (s ^+ (p ^ q)) . k = s ^ ((p ^ q) . k) by A2, Def2
.= s ^ (p . k) by A3, FINSEQ_1:def 7
.= (s ^+ p) . k by A3, Def2
.= ((s ^+ p) ^ (s ^+ q)) . k by A4, FINSEQ_1:def 7 ; :: thesis: verum

end;

suppose not k in dom p ; :: thesis: (s ^+ (p ^ q)) . k = ((s ^+ p) ^ (s ^+ q)) . k

then A5: ( k < 1 or k > len p ) by FINSEQ_3:27;
( 1 <= k & k <= len (p ^ q) ) by A2, FINSEQ_3:27;
then consider i being Nat such that
A6: ( k = (len p) + i & i >= 1 & i <= len q ) by A5, Th2;
A7: i in dom q by A6, FINSEQ_3:27;
then A8: i in dom (s ^+ q) by Def2;
A9: len (s ^+ p) = len p by Th5;
thus (s ^+ (p ^ q)) . k = s ^ ((p ^ q) . ((len p) + i)) by A2, A6, Def2
.= s ^ (q . i) by A7, FINSEQ_1:def 7
.= (s ^+ q) . i by A7, Def2
.= ((s ^+ p) ^ (s ^+ q)) . k by A6, A8, A9, FINSEQ_1:def 7 ; :: thesis: verum

end;

end;

end;

hence (s ^+ (p ^ q)) . k = ((s ^+ p) ^ (s ^+ q)) . k ; :: thesis: verum

end;

hence s ^+ (p ^ q) = (s ^+ p) ^ (s ^+ q) by A1, FINSEQ_1:17; :: thesis: (p ^ q) +^ s = (p +^ s) ^ (q +^ s)
len ((p ^ q) +^ s) = len (p ^ q) by Th5
.= (len p) + (len q) by FINSEQ_1:35
.= (len (p +^ s)) + (len q) by Th5
.= (len (p +^ s)) + (len (q +^ s)) by Th5
.= len ((p +^ s) ^ (q +^ s)) by FINSEQ_1:35 ;
then A10: dom ((p ^ q) +^ s) = dom ((p +^ s) ^ (q +^ s)) by FINSEQ_3:31;

now

let k be Nat; :: thesis: ( k in dom ((p ^ q) +^ s) implies ((p ^ q) +^ s) . k = ((p +^ s) ^ (q +^ s)) . k )
assume k in dom ((p ^ q) +^ s) ; :: thesis: ((p ^ q) +^ s) . k = ((p +^ s) ^ (q +^ s)) . k
then A11: k in dom (p ^ q) by Def3;

now

per cases ( k in dom p or not k in dom p ) ;

suppose A12: k in dom p ; :: thesis: ((p ^ q) +^ s) . k = ((p +^ s) ^ (q +^ s)) . k

then A13: k in dom (p +^ s) by Def3;
thus ((p ^ q) +^ s) . k = ((p ^ q) . k) ^ s by A11, Def3
.= (p . k) ^ s by A12, FINSEQ_1:def 7
.= (p +^ s) . k by A12, Def3
.= ((p +^ s) ^ (q +^ s)) . k by A13, FINSEQ_1:def 7 ; :: thesis: verum

end;

suppose not k in dom p ; :: thesis: ((p ^ q) +^ s) . k = ((p +^ s) ^ (q +^ s)) . k

then A14: ( k < 1 or k > len p ) by FINSEQ_3:27;
( 1 <= k & k <= len (p ^ q) ) by A11, FINSEQ_3:27;
then consider i being Nat such that
A15: ( k = (len p) + i & i >= 1 & i <= len q ) by A14, Th2;
A16: i in dom q by A15, FINSEQ_3:27;
then A17: i in dom (q +^ s) by Def3;
A18: len (p +^ s) = len p by Th5;
thus ((p ^ q) +^ s) . k = ((p ^ q) . ((len p) + i)) ^ s by A11, A15, Def3
.= (q . i) ^ s by A16, FINSEQ_1:def 7
.= (q +^ s) . i by A16, Def3
.= ((p +^ s) ^ (q +^ s)) . k by A15, A17, A18, FINSEQ_1:def 7 ; :: thesis: verum

end;

end;

end;

hence ((p ^ q) +^ s) . k = ((p +^ s) ^ (q +^ s)) . k ; :: thesis: verum

end;

hence (p ^ q) +^ s = (p +^ s) ^ (q +^ s) by A10, FINSEQ_1:17; :: thesis: verum