set X = INT ;
set Y = the Symbols of T;
A1: ex f being Function st
( t = f & dom f = INT & rng f c= the Symbols of T ) by FUNCT_2:def 2;
rng (h .--> s) = {s} by FUNCOP_1:8;
then ( rng (t +* (h .--> s)) c= (rng t) \/ (rng (h .--> s)) & (rng t) \/ (rng (h .--> s)) c= the Symbols of T ) by A1, FUNCT_4:17, XBOOLE_1:8;
then A2: rng (t +* (h .--> s)) c= the Symbols of T by XBOOLE_1:1;
A3: h in INT by INT_1:def 2;
dom (t +* (h .--> s)) = (dom t) \/ (dom (h .--> s)) by FUNCT_4:def 1
.= (dom t) \/ {h}
.= INT by A1, A3, ZFMISC_1:40 ;
hence t +* (h .--> s) is Tape of T by A2, FUNCT_2:def 2; :: thesis: verum