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 A2: s ^ u ==>* t ^ u,S by Th36;
t ^ u ==>* t ^ v,S by A1, Th36;
hence s ^ u ==>* t ^ v,S by A2, Th35; :: thesis: u ^ s ==>* v ^ t,S
A3: u ^ s ==>* u ^ t,S by A1, Th36;
u ^ t ==>* v ^ t,S by A1, Th36;
hence u ^ s ==>* v ^ t,S by A3, Th35; :: thesis: verum