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 ) )
proof
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;
3 in Seg 3 by FINSEQ_1:1;
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
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
.= X \ x by FINSEQ_1:45 ;
:: thesis: verum
end;
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 ) )
proof
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;
2 in Seg 3 by FINSEQ_1:1;
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
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
.= X \ y by FINSEQ_1:45 ;
:: thesis: verum
end;
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 )
proof
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;
assume q . 3 = FALSE ; :: thesis: (MergeSequence (<*x,y,z*>,q)) . 3 = X \ z
hence (MergeSequence (<*x,y,z*>,q)) . 3 = X \ (<*x,y,z*> . 3) by
.= X \ z by FINSEQ_1:45 ;
:: thesis: verum