let E be set ; :: thesis: for S being semi-Thue-system of E
for s, t, u, v being Element of E ^omega st s ==>* t,S & u ==>* v,S holds
( s ^ u ==>* t ^ v,S & u ^ s ==>* v ^ t,S )
let S be semi-Thue-system of E; :: thesis: for s, t, u, v being Element of E ^omega st s ==>* t,S & u ==>* v,S holds
( s ^ u ==>* t ^ v,S & u ^ s ==>* v ^ t,S )
let s, t, u, v be Element of E ^omega ; :: thesis: ( s ==>* t,S & u ==>* v,S implies ( s ^ u ==>* t ^ v,S & u ^ s ==>* v ^ t,S ) )
assume A1: ( s ==>* t,S & u ==>* v,S ) ; :: thesis: ( s ^ u ==>* t ^ v,S & u ^ s ==>* v ^ t,S )
then ( s ^ u ==>* t ^ u,S & t ^ u ==>* t ^ v,S ) by Th36;
hence s ^ u ==>* t ^ v,S by Th35; :: thesis: u ^ s ==>* v ^ t,S
( u ^ s ==>* u ^ t,S & u ^ t ==>* v ^ t,S ) by A1, Th36;
hence u ^ s ==>* v ^ t,S by Th35; :: thesis: verum