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

( t is Tape of tm1 & t is Tape of tm2 )

let t be Tape of (tm1 ';' tm2); :: thesis: ( the Symbols of tm1 = the Symbols of tm2 implies ( t is Tape of tm1 & t is Tape of 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 & t is Tape of 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 & t is Tape of tm2 ) by A1; :: thesis: verum

( t is Tape of tm1 & t is Tape of tm2 )

let t be Tape of (tm1 ';' tm2); :: thesis: ( the Symbols of tm1 = the Symbols of tm2 implies ( t is Tape of tm1 & t is Tape of 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 & t is Tape of 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 & t is Tape of tm2 ) by A1; :: thesis: verum