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 ) )

proof

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

end;

2 in Seg 2 by FINSEQ_1:3;
then A1: 2 in dom <*x,y*> by FINSEQ_3:29;
1 in Seg 2 by FINSEQ_1:3;
then A2: 1 in dom <*x,y*> by FINSEQ_3:29;
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

assume q . 1 = FALSE ; :: thesis: (MergeSequence <*x,y*>,q) . 1 = X \ x
hence (MergeSequence <*x,y*>,q) . 1 = X \ (<*x,y*> . 1) by A2, Th7
.= X \ x by FINSEQ_1:61 ;
:: thesis: verum

end;

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

proof

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

end;

assume q . 2 = FALSE ; :: thesis: (MergeSequence <*x,y*>,q) . 2 = X \ y
hence (MergeSequence <*x,y*>,q) . 2 = X \ (<*x,y*> . 2) by A1, Th7
.= X \ y by FINSEQ_1:61 ;
:: thesis: verum