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