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₁ being set holds
( not b₁ in J or C . b₁ c= A . 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