let S be set ; :: thesis: for s being FinSequence of S

for e being set st e in whole_event holds

ex x being Element of S st e in event_pick (x,s)

let s be FinSequence of S; :: thesis: for e being set st e in whole_event holds

ex x being Element of S st e in event_pick (x,s)

let e be set ; :: thesis: ( e in whole_event implies ex x being Element of S st e in event_pick (x,s) )

assume A1: e in whole_event ; :: thesis: ex x being Element of S st e in event_pick (x,s)

then e in s " S by RELSET_1:22;

then s . e in S by FUNCT_1:def 7;

then consider x being Element of S such that

A2: x = s . e ;

take x ; :: thesis: e in event_pick (x,s)

x in {x} by TARSKI:def 1;

hence e in event_pick (x,s) by A1, A2, FUNCT_1:def 7; :: thesis: verum

for e being set st e in whole_event holds

ex x being Element of S st e in event_pick (x,s)

let s be FinSequence of S; :: thesis: for e being set st e in whole_event holds

ex x being Element of S st e in event_pick (x,s)

let e be set ; :: thesis: ( e in whole_event implies ex x being Element of S st e in event_pick (x,s) )

assume A1: e in whole_event ; :: thesis: ex x being Element of S st e in event_pick (x,s)

then e in s " S by RELSET_1:22;

then s . e in S by FUNCT_1:def 7;

then consider x being Element of S such that

A2: x = s . e ;

take x ; :: thesis: e in event_pick (x,s)

x in {x} by TARSKI:def 1;

hence e in event_pick (x,s) by A1, A2, FUNCT_1:def 7; :: thesis: verum