let I be set ; :: thesis: for A being ManySortedSet of I
for B being non-empty ManySortedSet of I
for F being ManySortedFunction of A,B
for X being ManySortedSubset of A st A c= X holds
F || X = F
let A be ManySortedSet of I; :: thesis: for B being non-empty ManySortedSet of I
for F being ManySortedFunction of A,B
for X being ManySortedSubset of A st A c= X holds
F || X = F
let B be non-empty ManySortedSet of I; :: thesis: for F being ManySortedFunction of A,B
for X being ManySortedSubset of A st A c= X holds
F || X = F
let F be ManySortedFunction of A,B; :: thesis: for X being ManySortedSubset of A st A c= X holds
F || X = F
let X be ManySortedSubset of A; :: thesis: ( A c= X implies F || X = F )
assume A1: A c= X ; :: thesis: F || X = F

now :: thesis: for i being object st i in I holds
(F || X) . i = F . i

let i be object ; :: thesis: ( i in I implies (F || X) . i = F . i )
assume A2: i in I ; :: thesis: (F || X) . i = F . i
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def 15;
A3: A . i c= X . i by A1, A2;
thus (F || X) . i = f | (X . i) by A2, MSAFREE:def 1
.= F . i by A3, RELSET_1:19 ; :: thesis: verum

end;

hence F || X = F ; :: thesis: verum