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
A3: ( dom B1 = I1 & dom B2 = I2 ) by PARTFUN1:def 4;
reconsider H = Intersect F,G as ManySortedSet of by Th14;
A4: ( dom F = I1 & dom G = I2 ) by PARTFUN1:def 4;
A5: ( dom A1 = I1 & dom A2 = 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 M2( bool [:(A . i),(B . i):]) )
assume A6: i in I1 /\ I2 ; :: thesis: H . i is M2( bool [:(A . i),(B . i):])
then A7: H . i = (F . i) /\ (G . i) by A4, Def2;
A8: i in I2 by A6, XBOOLE_0:def 4;
then A9: G . i is Function of (A2 . i),(B2 . i) by PBOOLE:def 18;
A10: ( A . i = (A1 . i) /\ (A2 . i) & B . i = (B1 . i) /\ (B2 . i) ) by A1, A5, A3, A6, Def2;
A11: i in I1 by A6, XBOOLE_0:def 4;
then F . i is Function of (A1 . i),(B1 . i) by PBOOLE:def 18;
hence H . i is M2( bool [:(A . i),(B . i):]) by A2, A4, A11, A8, A10, A7, A9, FUNCT_2:197; :: thesis: verum

end;

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