let X be set ; :: thesis: 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; :: thesis: 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 ; :: thesis: ( ( 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 ) :: thesis: ( q . 1 = FALSE implies (MergeSequence (<*x*>,q)) . 1 = X \ x )

proof

assume q . 1 = TRUE ; :: thesis: (MergeSequence (<*x*>,q)) . 1 = x
hence (MergeSequence (<*x*>,q)) . 1 = <*x*> . 1 by Th6
.= x by FINSEQ_1:40 ;
:: thesis: verum

end;

1 in Seg 1 by FINSEQ_1:1;
then A1: 1 in dom <*x*> by FINSEQ_1:38;
assume q . 1 = FALSE ; :: thesis: (MergeSequence (<*x*>,q)) . 1 = X \ x
hence (MergeSequence (<*x*>,q)) . 1 = X \ (<*x*> . 1) by A1, Th7
.= X \ x by FINSEQ_1:40 ;
:: thesis: verum