let X be set ; :: thesis: for x, y being Subset of X

for q being FinSequence of BOOLEAN holds

( ( q . 1 = TRUE implies (MergeSequence (<*x,y*>,q)) . 1 = x ) & ( q . 1 = FALSE implies (MergeSequence (<*x,y*>,q)) . 1 = X \ x ) & ( q . 2 = TRUE implies (MergeSequence (<*x,y*>,q)) . 2 = y ) & ( q . 2 = FALSE implies (MergeSequence (<*x,y*>,q)) . 2 = X \ y ) )

let x, y be Subset of X; :: thesis: for q being FinSequence of BOOLEAN holds

( ( q . 1 = TRUE implies (MergeSequence (<*x,y*>,q)) . 1 = x ) & ( q . 1 = FALSE implies (MergeSequence (<*x,y*>,q)) . 1 = X \ x ) & ( q . 2 = TRUE implies (MergeSequence (<*x,y*>,q)) . 2 = y ) & ( q . 2 = FALSE implies (MergeSequence (<*x,y*>,q)) . 2 = X \ y ) )

let q be FinSequence of BOOLEAN ; :: thesis: ( ( q . 1 = TRUE implies (MergeSequence (<*x,y*>,q)) . 1 = x ) & ( q . 1 = FALSE implies (MergeSequence (<*x,y*>,q)) . 1 = X \ x ) & ( q . 2 = TRUE implies (MergeSequence (<*x,y*>,q)) . 2 = y ) & ( q . 2 = FALSE implies (MergeSequence (<*x,y*>,q)) . 2 = X \ y ) )

thus ( q . 1 = TRUE implies (MergeSequence (<*x,y*>,q)) . 1 = x ) :: thesis: ( ( q . 1 = FALSE implies (MergeSequence (<*x,y*>,q)) . 1 = X \ x ) & ( q . 2 = TRUE implies (MergeSequence (<*x,y*>,q)) . 2 = y ) & ( q . 2 = FALSE implies (MergeSequence (<*x,y*>,q)) . 2 = X \ y ) )

then A1: 2 in dom <*x,y*> by FINSEQ_1:89;

1 in Seg 2 by FINSEQ_1:1;

then A2: 1 in dom <*x,y*> by FINSEQ_1:89;

thus ( q . 1 = FALSE implies (MergeSequence (<*x,y*>,q)) . 1 = X \ x ) :: thesis: ( ( q . 2 = TRUE implies (MergeSequence (<*x,y*>,q)) . 2 = y ) & ( q . 2 = FALSE implies (MergeSequence (<*x,y*>,q)) . 2 = X \ y ) )

hence (MergeSequence (<*x,y*>,q)) . 2 = X \ (<*x,y*> . 2) by A1, Th3

.= X \ y by FINSEQ_1:44 ;

:: thesis: verum

for q being FinSequence of BOOLEAN holds

( ( q . 1 = TRUE implies (MergeSequence (<*x,y*>,q)) . 1 = x ) & ( q . 1 = FALSE implies (MergeSequence (<*x,y*>,q)) . 1 = X \ x ) & ( q . 2 = TRUE implies (MergeSequence (<*x,y*>,q)) . 2 = y ) & ( q . 2 = FALSE implies (MergeSequence (<*x,y*>,q)) . 2 = X \ y ) )

let x, y be Subset of X; :: thesis: for q being FinSequence of BOOLEAN holds

( ( q . 1 = TRUE implies (MergeSequence (<*x,y*>,q)) . 1 = x ) & ( q . 1 = FALSE implies (MergeSequence (<*x,y*>,q)) . 1 = X \ x ) & ( q . 2 = TRUE implies (MergeSequence (<*x,y*>,q)) . 2 = y ) & ( q . 2 = FALSE implies (MergeSequence (<*x,y*>,q)) . 2 = X \ y ) )

let q be FinSequence of BOOLEAN ; :: thesis: ( ( q . 1 = TRUE implies (MergeSequence (<*x,y*>,q)) . 1 = x ) & ( q . 1 = FALSE implies (MergeSequence (<*x,y*>,q)) . 1 = X \ x ) & ( q . 2 = TRUE implies (MergeSequence (<*x,y*>,q)) . 2 = y ) & ( q . 2 = FALSE implies (MergeSequence (<*x,y*>,q)) . 2 = X \ y ) )

thus ( q . 1 = TRUE implies (MergeSequence (<*x,y*>,q)) . 1 = x ) :: thesis: ( ( q . 1 = FALSE implies (MergeSequence (<*x,y*>,q)) . 1 = X \ x ) & ( q . 2 = TRUE implies (MergeSequence (<*x,y*>,q)) . 2 = y ) & ( q . 2 = FALSE implies (MergeSequence (<*x,y*>,q)) . 2 = X \ y ) )

proof

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

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

.= x by FINSEQ_1:44 ;

:: thesis: verum

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

.= x by FINSEQ_1:44 ;

:: thesis: verum

then A1: 2 in dom <*x,y*> by FINSEQ_1:89;

1 in Seg 2 by FINSEQ_1:1;

then A2: 1 in dom <*x,y*> by FINSEQ_1:89;

thus ( q . 1 = FALSE implies (MergeSequence (<*x,y*>,q)) . 1 = X \ x ) :: thesis: ( ( q . 2 = TRUE implies (MergeSequence (<*x,y*>,q)) . 2 = y ) & ( q . 2 = FALSE implies (MergeSequence (<*x,y*>,q)) . 2 = X \ y ) )

proof

thus
( q . 2 = TRUE implies (MergeSequence (<*x,y*>,q)) . 2 = y )
:: thesis: ( q . 2 = FALSE implies (MergeSequence (<*x,y*>,q)) . 2 = X \ y )
assume
q . 1 = FALSE
; :: thesis: (MergeSequence (<*x,y*>,q)) . 1 = X \ x

hence (MergeSequence (<*x,y*>,q)) . 1 = X \ (<*x,y*> . 1) by A2, Th3

.= X \ x by FINSEQ_1:44 ;

:: thesis: verum

end;hence (MergeSequence (<*x,y*>,q)) . 1 = X \ (<*x,y*> . 1) by A2, Th3

.= X \ x by FINSEQ_1:44 ;

:: thesis: verum

proof

assume
q . 2 = FALSE
; :: thesis: (MergeSequence (<*x,y*>,q)) . 2 = X \ y
assume
q . 2 = TRUE
; :: thesis: (MergeSequence (<*x,y*>,q)) . 2 = y

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

.= y by FINSEQ_1:44 ;

:: thesis: verum

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

.= y by FINSEQ_1:44 ;

:: thesis: verum

hence (MergeSequence (<*x,y*>,q)) . 2 = X \ (<*x,y*> . 2) by A1, Th3

.= X \ y by FINSEQ_1:44 ;

:: thesis: verum