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

for q being FinSequence of BOOLEAN holds

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

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

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

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

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

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

1 in Seg 3 by FINSEQ_1:1;

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

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

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

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

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

.= X \ z by FINSEQ_1:45 ;

:: thesis: verum

for q being FinSequence of BOOLEAN holds

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

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

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

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

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

proof

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

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

.= x by FINSEQ_1:45 ;

:: thesis: verum

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

.= x by FINSEQ_1:45 ;

:: thesis: verum

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

1 in Seg 3 by FINSEQ_1:1;

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

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

proof

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

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

.= X \ x by FINSEQ_1:45 ;

:: thesis: verum

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

.= X \ x by FINSEQ_1:45 ;

:: thesis: verum

proof

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

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

.= y by FINSEQ_1:45 ;

:: thesis: verum

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

.= y by FINSEQ_1:45 ;

:: thesis: verum

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

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

proof

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

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

.= X \ y by FINSEQ_1:45 ;

:: thesis: verum

end;hence (MergeSequence (<*x,y,z*>,q)) . 2 = X \ (<*x,y,z*> . 2) by A3, Th3

.= X \ y by FINSEQ_1:45 ;

:: thesis: verum

proof

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

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

.= z by FINSEQ_1:45 ;

:: thesis: verum

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

.= z by FINSEQ_1:45 ;

:: thesis: verum

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

.= X \ z by FINSEQ_1:45 ;

:: thesis: verum