let I1, I2 be set ; :: thesis: for A1, B1 being ManySortedSet of
for A2, B2 being ManySortedSet of
for A, B being ManySortedSet of 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
let A1, B1 be ManySortedSet of ; :: thesis: for A2, B2 being ManySortedSet of
for A, B being ManySortedSet of 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
let A2, B2 be ManySortedSet of ; :: thesis: for A, B being ManySortedSet of 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
let A, B be ManySortedSet of ; :: thesis: ( A = Intersect A1,A2 & B = Intersect B1,B2 implies 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 )
assume A1: ( A = Intersect A1,A2 & B = Intersect B1,B2 ) ; :: thesis: 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
let F be ManySortedFunction of A1,B1; :: thesis: 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
let G be ManySortedFunction of A2,B2; :: thesis: ( ( for x being set st x in dom F & x in dom G holds
F . x tolerates G . x ) implies Intersect F,G is ManySortedFunction of A,B )
assume A2: for x being set st x in dom F & x in dom G holds
F . x tolerates G . x ; :: thesis: Intersect F,G is ManySortedFunction of A,B
reconsider H = Intersect F,G as ManySortedSet of by Th14;
A3: ( dom F = I1 & dom G = I2 & dom A1 = I1 & dom A2 = I2 & dom A = I1 /\ I2 & dom B1 = I1 & dom B2 = I2 & dom B = I1 /\ I2 ) by PARTFUN1:def 4;
H is ManySortedFunction of A,B

proof

let i be set ; :: according to PBOOLE:def 18 :: thesis: ( not i in I1 /\ I2 or H . i is Element of bool [:(A . i),(B . i):] )
assume i in I1 /\ I2 ; :: thesis: H . i is Element of bool [:(A . i),(B . i):]
then A4: ( i in I1 & i in I2 & A . i = (A1 . i) /\ (A2 . i) & B . i = (B1 . i) /\ (B2 . i) & H . i = (F . i) /\ (G . i) ) by A1, A3, Def2, XBOOLE_0:def 4;
then ( F . i is Function of (A1 . i),(B1 . i) & G . i is Function of (A2 . i),(B2 . i) & F . i tolerates G . i ) by A2, A3, PBOOLE:def 18;
hence H . i is Element of bool [:(A . i),(B . i):] by A4, FUNCT_2:197; :: thesis: verum

end;

hence Intersect F,G is ManySortedFunction of A,B ; :: thesis: verum