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

proof

let x be set ; :: 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 ZZ: 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 ZZ, Th23;

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 F; :: thesis: verum

end;

end;

end;

assume Z: ( 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 Z;

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

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

end;

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

then ex M being Element of NAT st
( x = M + (card p) & M in dom q ) by F;
hence x in dom (p ^ q) by Th26; :: thesis: verum

end;

end;

end;

then A: dom (p ^ q) = (dom p) \/ (dom (Shift (q,(card p)))) by XBOOLE_0:def 3;
for x being set 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 set ; :: 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 Z: 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 ZZ: 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 Element of NAT such that
W1: x = M + (card p) and
W2: M in dom q by ZZ, F;
set m = k -' (len p);
A: (len p) + (k -' (len p)) = k by NAT_D:34, W1;
hence (p ^ q) . x = q . (k -' (len p)) by W1, W2, Def4
.= (Shift (q,(card p))) . x by W1, W2, A, 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 Z, XBOOLE_0:def 3;
hence (p ^ q) . x = p . x by Def4; :: thesis: verum

end;

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