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 )

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, Th3

.= X \ x by FINSEQ_1:40 ;

:: thesis: verum

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

1 in Seg 1
by FINSEQ_1:1;
assume
q . 1 = TRUE
; :: thesis: (MergeSequence (<*x*>,q)) . 1 = x

hence (MergeSequence (<*x*>,q)) . 1 = <*x*> . 1 by Th2

.= x by FINSEQ_1:40 ;

:: thesis: verum

end;hence (MergeSequence (<*x*>,q)) . 1 = <*x*> . 1 by Th2

.= x by FINSEQ_1:40 ;

:: thesis: verum

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, Th3

.= X \ x by FINSEQ_1:40 ;

:: thesis: verum