let I be set ; :: thesis: for M being ManySortedSet of I
for SF being non empty SubsetFamily of M holds dom |.SF.| = I
let M be ManySortedSet of I; :: thesis: for SF being non empty SubsetFamily of M holds dom |.SF.| = I
let SF be non empty SubsetFamily of M; :: thesis: dom |.SF.| = I
consider A being non empty functional set such that
A1: A = SF and
A2: dom |.SF.| = meet { (dom x) where x is Element of A : verum } and
for i being set st i in dom |.SF.| holds
|.SF.| . i = { (x . i) where x is Element of A : verum } by Def2;
{ (dom x) where x is Element of A : verum } = {I}

proof

thus { (dom x) where x is Element of A : verum } c= {I} :: according to XBOOLE_0:def 10 :: thesis: {I} c= { (dom x) where x is Element of A : verum }

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (dom x) where x is Element of A : verum } or a in {I} )
assume a in { (dom x) where x is Element of A : verum } ; :: thesis: a in {I}
then consider x being Element of A such that
A3: a = dom x ;
x is Element of SF by A1;
then a = I by A3, PARTFUN1:def 2;
hence a in {I} by TARSKI:def 1; :: thesis: verum

end;

set x = the Element of A;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in {I} or a in { (dom x) where x is Element of A : verum } )
assume a in {I} ; :: thesis: a in { (dom x) where x is Element of A : verum }
then A4: a = I by TARSKI:def 1;
the Element of A is Element of SF by A1;
then dom the Element of A = I by PARTFUN1:def 2;
hence a in { (dom x) where x is Element of A : verum } by A4; :: thesis: verum

end;

hence dom |.SF.| = I by A2, SETFAM_1:10; :: thesis: verum