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