let I be set ; :: thesis: for X being V8() ManySortedSet of I ex x being ManySortedSet of I st x in X
let X be V8() ManySortedSet of I; :: thesis: ex x being ManySortedSet of I 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 I 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 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