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

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