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