let I be set ; :: thesis: for A being ManySortedSet of I ex R being ManySortedRelation of A st
( R = I --> {} & R is terminating )
let A be ManySortedSet of I; :: thesis: ex R being ManySortedRelation of A st
( R = I --> {} & R is terminating )
set R = I --> {};
for i being set st i in I holds
(I --> {}) . i is Relation of (A . i) by XBOOLE_1:2;
then reconsider R = I --> {} as ManySortedRelation of A by MSUALG_4:def 1;
take R ; :: thesis: ( R = I --> {} & R is terminating )
thus R = I --> {} ; :: thesis: R is terminating
let i be set ; :: according to MSAFREE4:def 16 :: thesis: ( i in I implies R . i is strongly-normalizing )
thus ( i in I implies R . i is strongly-normalizing ) ; :: thesis: verum