let I1, I2 be set ; :: thesis: 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

let A1, B1 be ManySortedSet of I1; :: thesis: 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

let A2, B2 be ManySortedSet of I2; :: thesis: 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

let A, B be ManySortedSet of I1 /\ I2; :: 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 2;

reconsider H = Intersect (F,G) as ManySortedSet of I1 /\ I2 by Th14;

A4: ( dom F = I1 & dom G = I2 ) by PARTFUN1:def 2;

A5: ( dom A1 = I1 & dom A2 = I2 ) by PARTFUN1:def 2;

H is ManySortedFunction of A,B

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

let A1, B1 be ManySortedSet of I1; :: thesis: 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

let A2, B2 be ManySortedSet of I2; :: thesis: 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

let A, B be ManySortedSet of I1 /\ I2; :: 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 2;

reconsider H = Intersect (F,G) as ManySortedSet of I1 /\ I2 by Th14;

A4: ( dom F = I1 & dom G = I2 ) by PARTFUN1:def 2;

A5: ( dom A1 = I1 & dom A2 = I2 ) by PARTFUN1:def 2;

H is ManySortedFunction of A,B

proof

hence
Intersect (F,G) is ManySortedFunction of A,B
; :: thesis: verum
let i be object ; :: according to PBOOLE:def 15 :: thesis: ( not i in I1 /\ I2 or H . i is M3( bool [:(A . i),(B . i):]) )

assume A6: i in I1 /\ I2 ; :: thesis: H . i is M3( 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 15;

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 15;

hence H . i is M3( bool [:(A . i),(B . i):]) by A2, A4, A11, A8, A10, A7, A9, FUNCT_2:120; :: thesis: verum

end;assume A6: i in I1 /\ I2 ; :: thesis: H . i is M3( 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 15;

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 15;

hence H . i is M3( bool [:(A . i),(B . i):]) by A2, A4, A11, A8, A10, A7, A9, FUNCT_2:120; :: thesis: verum