let S be non empty non void ManySortedSign ; :: thesis: for X being ManySortedSet of the carrier of S
for o, b being object 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 object 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 object ; :: 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:87;
reconsider b9 = b as Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * by A1, ZFMISC_1:87;
A2: [o9,b9] in REL X by A1;
hence o in [: the carrier' of S,{ the carrier of S}:] by MSAFREE:def 7; :: 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