let p, q be 1-sorted-yielding FinSequence; :: thesis: Carrier (p ^ q) = (Carrier p) ^ (Carrier q)
A1: len (Carrier (p ^ q)) = len (p ^ q) by Th13
.= (len p) + (len q) by FINSEQ_1:22
.= (len (Carrier p)) + (len q) by Th13
.= (len (Carrier p)) + (len (Carrier q)) by Th13
.= len ((Carrier p) ^ (Carrier q)) by FINSEQ_1:22 ;

now :: thesis: for k being Nat st 1 <= k & k <= len (Carrier (p ^ q)) holds
(Carrier (p ^ q)) . k = ((Carrier p) ^ (Carrier q)) . k

let k be Nat; :: thesis: ( 1 <= k & k <= len (Carrier (p ^ q)) implies (Carrier (p ^ q)) . b₁ = ((Carrier p) ^ (Carrier q)) . b₁ )
assume ( 1 <= k & k <= len (Carrier (p ^ q)) ) ; :: thesis: (Carrier (p ^ q)) . b₁ = ((Carrier p) ^ (Carrier q)) . b₁
then k in dom (Carrier (p ^ q)) by FINSEQ_3:25;
then A3: k in dom (p ^ q) by Def13;
then consider R being 1-sorted such that
A4: ( R = (p ^ q) . k & (Carrier (p ^ q)) . k = the carrier of R ) by Def13;

per cases ( k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) ) by A3, FINSEQ_1:25;

suppose A5: k in dom p ; :: thesis: (Carrier (p ^ q)) . b₁ = ((Carrier p) ^ (Carrier q)) . b₁

then consider R9 being 1-sorted such that
A6: ( R9 = p . k & (Carrier p) . k = the carrier of R9 ) by Def13;
A7: k in dom (Carrier p) by A5, Def13;
R = R9 by A4, A5, A6, FINSEQ_1:def 7;
hence (Carrier (p ^ q)) . k = ((Carrier p) ^ (Carrier q)) . k by A4, A6, A7, FINSEQ_1:def 7; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom q & k = (len p) + n ) ; :: thesis: (Carrier (p ^ q)) . b₁ = ((Carrier p) ^ (Carrier q)) . b₁

then consider n being Nat such that
A8: ( n in dom q & k = (len p) + n ) ;
consider R9 being 1-sorted such that
A9: ( R9 = q . n & (Carrier q) . n = the carrier of R9 ) by A8, Def13;
A10: ( n in dom (Carrier q) & k = (len (Carrier p)) + n ) by A8, Th13, Def13;
R = R9 by A4, A8, A9, FINSEQ_1:def 7;
hence (Carrier (p ^ q)) . k = ((Carrier p) ^ (Carrier q)) . k by A4, A9, A10, FINSEQ_1:def 7; :: thesis: verum

end;

end;

end;

hence Carrier (p ^ q) = (Carrier p) ^ (Carrier q) by A1, FINSEQ_1:def 18; :: thesis: verum