let I be set ; :: thesis: for A being ManySortedSet of
for B being V2() ManySortedSet of
for F being ManySortedFunction of A,B
for X being ManySortedSubset of A holds doms (F || X) c= doms F
let A be ManySortedSet of ; :: thesis: for B being V2() ManySortedSet of
for F being ManySortedFunction of A,B
for X being ManySortedSubset of A holds doms (F || X) c= doms F
let B be V2() ManySortedSet of ; :: thesis: for F being ManySortedFunction of A,B
for X being ManySortedSubset of A holds doms (F || X) c= doms F
let F be ManySortedFunction of A,B; :: thesis: for X being ManySortedSubset of A holds doms (F || X) c= doms F
let X be ManySortedSubset of A; :: thesis: doms (F || X) c= doms F
let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or (doms (F || X)) . i c= (doms F) . i )
assume A1: i in I ; :: thesis: (doms (F || X)) . i c= (doms F) . i
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def 18;
dom F = I by PARTFUN1:def 4;
then A2: (doms F) . i = dom f by A1, FUNCT_6:31;
A3: (F || X) . i = f | (X . i) by A1, MSAFREE:def 1;
dom (F || X) = I by PARTFUN1:def 4;
then (doms (F || X)) . i = dom (f | (X . i)) by A1, A3, FUNCT_6:31;
hence (doms (F || X)) . i c= (doms F) . i by A2, RELAT_1:89; :: thesis: verum