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 --> {};

now :: thesis: for i being set st i in I holds
(I --> {}) . i is Relation of (A . i)

let i be set ; :: thesis: ( i in I implies (I --> {}) . i is Relation of (A . i) )
assume i in I ; :: thesis: (I --> {}) . i is Relation of (A . i)
then (I --> {}) . i = {} by FUNCOP_1:7;
hence (I --> {}) . i is Relation of (A . i) by XBOOLE_1:2; :: thesis: verum

end;

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 13 :: thesis: ( i in I implies R . i is strongly-normalizing )
assume i in I ; :: thesis: R . i is strongly-normalizing
hence R . i is strongly-normalizing by FUNCOP_1:7; :: thesis: verum