let I be set ; :: thesis: for X being non-empty ManySortedSet of I ex x being ManySortedSet of I st x in X
let X be non-empty ManySortedSet of I; :: thesis: ex x being ManySortedSet of I st x in X
deffunc H₁( object ) -> set = X . $1;
A1: for i being object st i in I holds
H₁(i) <> {} by Def13;
consider f being ManySortedSet of I such that
A2: for i being object st i in I holds
f . i in H₁(i) from PBOOLE:sch 1(A1);
take f ; :: thesis: f in X
let i be object ; :: according to PBOOLE:def 1 :: thesis: ( i in I implies f . i in X . i )
thus ( i in I implies f . i in X . i ) by A2; :: thesis: verum