let S be non empty finite set ; :: thesis: for X being Subset of S
for s being FinSequence of S holds s " X = trueEVENT ((MembershipDecision X) * s)
let X be Subset of S; :: thesis: for s being FinSequence of S holds s " X = trueEVENT ((MembershipDecision X) * s)
let s be FinSequence of S; :: thesis: s " X = trueEVENT ((MembershipDecision X) * s)
set SX = s " X;
reconsider SX = s " X as Subset of (dom s) by RELAT_1:132;
dom ((MembershipDecision X) * s) c= dom s by RELAT_1:25;
then reconsider SY = trueEVENT ((MembershipDecision X) * s) as Subset of (dom s) by XBOOLE_1:1;
consider f being Function of S,BOOLEAN such that
A1: ( f = chi (X,S) & MembershipDecision X = f ) ;
A2: dom f = S by A1, FUNCT_3:def 3;
A3: for x being object st x in SY holds
x in SX
proof
let x be object ; :: thesis: ( x in SY implies x in SX )
assume A4: x in SY ; :: thesis: x in SX
s . x in trueEVENT f by A1, Th13, A4;
then ( s . x in dom f & f . (s . x) in {TRUE} ) by FUNCT_1:def 7;
then ( s . x in dom f & f . (s . x) = TRUE ) by TARSKI:def 1;
then s . x in X by A1, FUNCT_3:36;
hence x in SX by A4, FUNCT_1:def 7; :: thesis: verum
end;
for x being object st x in SX holds
x in SY
proof
let x be object ; :: thesis: ( x in SX implies x in SY )
assume A5: x in SX ; :: thesis: x in SY
A6: s . x in rng s by A5, FUNCT_1:3;
s . x in X by A5, FUNCT_1:def 7;
then f . (s . x) = TRUE by A1, FUNCT_3:def 3;
then f . (s . x) in {TRUE} by TARSKI:def 1;
then s . x in trueEVENT f by A6, A2, FUNCT_1:def 7;
hence x in SY by A1, Th13, A5; :: thesis: verum
end;
hence s " X = trueEVENT ((MembershipDecision X) * s) by A3, TARSKI:2; :: thesis: verum