let tm1, tm2 be TuringStr ; :: thesis: for t being Tape of tm1 st the Symbols of tm1 = the Symbols of tm2 holds

t is Tape of (tm1 ';' tm2)

let t be Tape of tm1; :: thesis: ( the Symbols of tm1 = the Symbols of tm2 implies t is Tape of (tm1 ';' tm2) )

set S1 = the Symbols of tm1;

set S2 = the Symbols of tm2;

assume A1: the Symbols of tm1 = the Symbols of tm2 ; :: thesis: t is Tape of (tm1 ';' tm2)

the Symbols of (tm1 ';' tm2) = the Symbols of tm1 \/ the Symbols of tm2 by Def31

.= the Symbols of tm1 by A1 ;

hence t is Tape of (tm1 ';' tm2) ; :: thesis: verum

t is Tape of (tm1 ';' tm2)

let t be Tape of tm1; :: thesis: ( the Symbols of tm1 = the Symbols of tm2 implies t is Tape of (tm1 ';' tm2) )

set S1 = the Symbols of tm1;

set S2 = the Symbols of tm2;

assume A1: the Symbols of tm1 = the Symbols of tm2 ; :: thesis: t is Tape of (tm1 ';' tm2)

the Symbols of (tm1 ';' tm2) = the Symbols of tm1 \/ the Symbols of tm2 by Def31

.= the Symbols of tm1 by A1 ;

hence t is Tape of (tm1 ';' tm2) ; :: thesis: verum