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
proof
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;
hence Intersect (F,G) is ManySortedFunction of A,B ; :: thesis: verum