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