let I, J be set ; :: thesis: for A being ManySortedSet of I

for B being Function

for C being ManySortedSet of J st C = Intersect (A,B) holds

C cc= A

let A be ManySortedSet of I; :: thesis: for B being Function

for C being ManySortedSet of J st C = Intersect (A,B) holds

C cc= A

let B be Function; :: thesis: for C being ManySortedSet of J st C = Intersect (A,B) holds

C cc= A

let C be ManySortedSet of J; :: thesis: ( C = Intersect (A,B) implies C cc= A )

assume A1: C = Intersect (A,B) ; :: thesis: C cc= A

A2: dom A = I by PARTFUN1:def 2;

dom C = J by PARTFUN1:def 2;

then A3: J = I /\ (dom B) by A1, A2, Def2;

hence J c= I by XBOOLE_1:17; :: according to ALTCAT_2:def 2 :: thesis: for b_{1} being set holds

( not b_{1} in J or C . b_{1} c= A . b_{1} )

let i be set ; :: thesis: ( not i in J or C . i c= A . i )

assume i in J ; :: thesis: C . i c= A . i

then C . i = (A . i) /\ (B . i) by A1, A2, A3, Def2;

hence C . i c= A . i by XBOOLE_1:17; :: thesis: verum

for B being Function

for C being ManySortedSet of J st C = Intersect (A,B) holds

C cc= A

let A be ManySortedSet of I; :: thesis: for B being Function

for C being ManySortedSet of J st C = Intersect (A,B) holds

C cc= A

let B be Function; :: thesis: for C being ManySortedSet of J st C = Intersect (A,B) holds

C cc= A

let C be ManySortedSet of J; :: thesis: ( C = Intersect (A,B) implies C cc= A )

assume A1: C = Intersect (A,B) ; :: thesis: C cc= A

A2: dom A = I by PARTFUN1:def 2;

dom C = J by PARTFUN1:def 2;

then A3: J = I /\ (dom B) by A1, A2, Def2;

hence J c= I by XBOOLE_1:17; :: according to ALTCAT_2:def 2 :: thesis: for b

( not b

let i be set ; :: thesis: ( not i in J or C . i c= A . i )

assume i in J ; :: thesis: C . i c= A . i

then C . i = (A . i) /\ (B . i) by A1, A2, A3, Def2;

hence C . i c= A . i by XBOOLE_1:17; :: thesis: verum