let S be non empty non void ManySortedSign ; :: thesis: for X being ManySortedSet of the carrier of S
for o, b being set st [o,b] in REL X holds
( o in [:the carrier' of S,{the carrier of S}:] & b in ([:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X))) * )
let X be ManySortedSet of the carrier of S; :: thesis: for o, b being set st [o,b] in REL X holds
( o in [:the carrier' of S,{the carrier of S}:] & b in ([:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X))) * )
let o, b be set ; :: thesis: ( [o,b] in REL X implies ( o in [:the carrier' of S,{the carrier of S}:] & b in ([:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X))) * ) )
assume A1: [o,b] in REL X ; :: thesis: ( o in [:the carrier' of S,{the carrier of S}:] & b in ([:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X))) * )
then reconsider o9 = o as Element of [:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X)) by ZFMISC_1:106;
reconsider b9 = b as Element of ([:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X))) * by A1, ZFMISC_1:106;
A2: [o9,b9] in REL X by A1;
hence o in [:the carrier' of S,{the carrier of S}:] by MSAFREE:def 9; :: thesis: b in ([:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X))) *
thus b in ([:the carrier' of S,{the carrier of S}:] \/ (Union (coprod X))) * by A2; :: thesis: verum