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

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