let X be set ; for x being Subset of X
for q being FinSequence of BOOLEAN holds
( ( q . 1 = TRUE implies (MergeSequence (<*x*>,q)) . 1 = x ) & ( q . 1 = FALSE implies (MergeSequence (<*x*>,q)) . 1 = X \ x ) )
let x be Subset of X; for q being FinSequence of BOOLEAN holds
( ( q . 1 = TRUE implies (MergeSequence (<*x*>,q)) . 1 = x ) & ( q . 1 = FALSE implies (MergeSequence (<*x*>,q)) . 1 = X \ x ) )
let q be FinSequence of BOOLEAN ; ( ( q . 1 = TRUE implies (MergeSequence (<*x*>,q)) . 1 = x ) & ( q . 1 = FALSE implies (MergeSequence (<*x*>,q)) . 1 = X \ x ) )
thus
( q . 1 = TRUE implies (MergeSequence (<*x*>,q)) . 1 = x )
( q . 1 = FALSE implies (MergeSequence (<*x*>,q)) . 1 = X \ x )
1 in Seg 1
by FINSEQ_1:1;
then A1:
1 in dom <*x*>
by FINSEQ_1:38;
assume
q . 1 = FALSE
; (MergeSequence (<*x*>,q)) . 1 = X \ x
hence (MergeSequence (<*x*>,q)) . 1 =
X \ (<*x*> . 1)
by A1, Th3
.=
X \ x
by FINSEQ_1:40
;
verum