theorem Th16:
for
I1,
I2 being
set for
A1,
B1 being
ManySortedSet of
I1 for
A2,
B2 being
ManySortedSet of
I2 for
A,
B being
ManySortedSet of
I1 /\ I2 st
A = Intersect (
A1,
A2) &
B = Intersect (
B1,
B2) holds
for
F being
ManySortedFunction of
A1,
B1 for
G being
ManySortedFunction of
A2,
B2 st ( for
x being
set st
x in dom F &
x in dom G holds
F . x tolerates G . x ) holds
Intersect (
F,
G) is
ManySortedFunction of
A,
B