let p, q be XFinSequence; :: thesis: p ^ q = p +* (Shift (q,(card p)))
A1: dom (Shift (q,(card p))) = { (M + (card p)) where M is Nat : M in dom q } by VALUED_1:def 12;
for x being object holds
( x in dom (p ^ q) iff ( x in dom p or x in dom (Shift (q,(card p))) ) )

proof

let x be object ; :: thesis: ( x in dom (p ^ q) iff ( x in dom p or x in dom (Shift (q,(card p))) ) )
thus ( not x in dom (p ^ q) or x in dom p or x in dom (Shift (q,(card p))) ) :: thesis: ( ( x in dom p or x in dom (Shift (q,(card p))) ) implies x in dom (p ^ q) )

proof

assume A2: x in dom (p ^ q) ; :: thesis: ( x in dom p or x in dom (Shift (q,(card p))) )
then reconsider k = x as Nat ;

per cases ( k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) ) by A2, Th18;

suppose k in dom p ; :: thesis: ( x in dom p or x in dom (Shift (q,(card p))) )

hence ( x in dom p or x in dom (Shift (q,(card p))) ) ; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom q & k = (len p) + n ) ; :: thesis: ( x in dom p or x in dom (Shift (q,(card p))) )

hence ( x in dom p or x in dom (Shift (q,(card p))) ) by A1; :: thesis: verum

end;

end;

end;

assume A3: ( x in dom p or x in dom (Shift (q,(card p))) ) ; :: thesis: x in dom (p ^ q)

per cases ( x in dom p or x in dom (Shift (q,(card p))) ) by A3;

suppose A4: x in dom p ; :: thesis: x in dom (p ^ q)

dom p c= dom (p ^ q) by Th19;
hence x in dom (p ^ q) by A4; :: thesis: verum

end;

suppose x in dom (Shift (q,(card p))) ; :: thesis: x in dom (p ^ q)

then ex M being Nat st
( x = M + (card p) & M in dom q ) by A1;
hence x in dom (p ^ q) by Th21; :: thesis: verum

end;

end;

end;

then A5: dom (p ^ q) = (dom p) \/ (dom (Shift (q,(card p)))) by XBOOLE_0:def 3;
for x being object st x in (dom p) \/ (dom (Shift (q,(card p)))) holds
( ( x in dom (Shift (q,(card p))) implies (p ^ q) . x = (Shift (q,(card p))) . x ) & ( not x in dom (Shift (q,(card p))) implies (p ^ q) . x = p . x ) )

proof

let x be object ; :: thesis: ( x in (dom p) \/ (dom (Shift (q,(card p)))) implies ( ( x in dom (Shift (q,(card p))) implies (p ^ q) . x = (Shift (q,(card p))) . x ) & ( not x in dom (Shift (q,(card p))) implies (p ^ q) . x = p . x ) ) )
assume A6: x in (dom p) \/ (dom (Shift (q,(card p)))) ; :: thesis: ( ( x in dom (Shift (q,(card p))) implies (p ^ q) . x = (Shift (q,(card p))) . x ) & ( not x in dom (Shift (q,(card p))) implies (p ^ q) . x = p . x ) )

hereby :: thesis: ( not x in dom (Shift (q,(card p))) implies (p ^ q) . x = p . x )

assume A7: x in dom (Shift (q,(card p))) ; :: thesis: (p ^ q) . x = (Shift (q,(card p))) . x
then reconsider k = x as Nat ;
consider M being Nat such that
A8: x = M + (card p) and
A9: M in dom q by A7, A1;
set m = k -' (len p);
A10: (len p) + (k -' (len p)) = k by A8, NAT_D:34;
hence (p ^ q) . x = q . (k -' (len p)) by A8, A9, Def3
.= (Shift (q,(card p))) . x by A8, A9, A10, VALUED_1:def 12 ;
:: thesis: verum

end;

assume not x in dom (Shift (q,(card p))) ; :: thesis: (p ^ q) . x = p . x
then x in dom p by A6, XBOOLE_0:def 3;
hence (p ^ q) . x = p . x by Def3; :: thesis: verum

end;

hence p ^ q = p +* (Shift (q,(card p))) by A5, FUNCT_4:def 1; :: thesis: verum