let I be set ; for A being ManySortedSet of I
for B being V2() ManySortedSet of I
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 I; for B being V2() ManySortedSet of I
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 I; 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; for X being ManySortedSubset of A holds doms (F || X) c= doms F
let X be ManySortedSubset of A; doms (F || X) c= doms F
let i be object ; PBOOLE:def 2 ( not i in I or (doms (F || X)) . i c= (doms F) . i )
A1:
dom (F || X) = I
by PARTFUN1:def 2;
assume A2:
i in I
; (doms (F || X)) . i c= (doms F) . i
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def 15;
dom F = I
by PARTFUN1:def 2;
then A3:
(doms F) . i = dom f
by A2, FUNCT_6:22;
(F || X) . i = f | (X . i)
by A2, MSAFREE:def 1;
then
(doms (F || X)) . i = dom (f | (X . i))
by A2, A1, FUNCT_6:22;
hence
(doms (F || X)) . i c= (doms F) . i
by A3, RELAT_1:60; verum