environ
vocabularies HIDDEN, NUMBERS, NAT_1, XBOOLE_0, FINSEQ_1, FUNCT_1, RELAT_1, TARSKI, SUBSET_1, MARGREL1, FINSET_1, FINSEQ_2, CARD_1, SETFAM_1, STRUCT_0, ZFMISC_1, FUNCOP_1, XBOOLEAN, EQREL_1, ORDERS_2, WAYBEL23, YELLOW_0, LATTICES, ORDINAL2, WAYBEL_0, WAYBEL_3, WAYBEL_8, RCOMP_1, PRE_TOPC, RLVECT_3, CANTOR_1, YELLOW15;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, SETFAM_1, DOMAIN_1, CARD_1, NUMBERS, FINSET_1, STRUCT_0, MARGREL1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSEQ_4, EQREL_1, FUNCOP_1, CARD_3, PRE_TOPC, TOPS_2, CANTOR_1, ORDERS_2, YELLOW_0, WAYBEL_0, WAYBEL_3, WAYBEL_8, WAYBEL23;
definitions TARSKI, FUNCT_1, XBOOLE_0, MARGREL1;
theorems TARSKI, SETFAM_1, ZFMISC_1, FINSET_1, RELAT_1, FUNCT_1, FUNCT_2, MSSUBFAM, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, EQREL_1, FUNCOP_1, CARD_1, CARD_4, T_0TOPSP, PRE_TOPC, TOPS_2, CANTOR_1, YELLOW_0, YELLOW_8, YELLOW_9, WAYBEL_0, WAYBEL_3, WAYBEL_8, WAYBEL23, XBOOLE_0, XBOOLE_1, SUBSET_1, ORDINAL1, XBOOLEAN;
schemes FUNCT_2, PRE_CIRC, FINSEQ_1, FRAENKEL;
registrations SUBSET_1, FUNCT_1, RELSET_1, FINSET_1, FINSEQ_1, MARGREL1, FINSEQ_2, STRUCT_0, TOPS_1, LATTICE3, WAYBEL_0, WAYBEL_3, WAYBEL23, ORDINAL1, PRE_TOPC, ZFMISC_1, CARD_1, RELAT_1, FINSEQ_3;
constructors HIDDEN, XXREAL_0, FINSEQ_4, REALSET1, VALUAT_1, TOPS_2, CANTOR_1, WAYBEL_8, WAYBEL23, RELSET_1, NUMBERS;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE;
equalities XBOOLE_0, MARGREL1, XBOOLEAN, STRUCT_0;
expansions TARSKI, XBOOLE_0;
scheme
SeqLambda1C{
F1()
-> Nat,
F2()
-> non
empty set ,
P1[
object ],
F3(
object )
-> set ,
F4(
object )
-> set } :
ex
p being
FinSequence of
F2() st
(
len p = F1() & ( for
i being
Nat st
i in Seg F1() holds
( (
P1[
i] implies
p . i = F3(
i) ) & (
P1[
i] implies
p . i = F4(
i) ) ) ) )
provided
A1:
for
i being
Nat st
i in Seg F1() holds
( (
P1[
i] implies
F3(
i)
in F2() ) & (
P1[
i] implies
F4(
i)
in F2() ) )
definition
let X be
set ;
let p be
FinSequence of
bool X;
let q be
FinSequence of
BOOLEAN ;
existence
ex b1 being FinSequence of bool X st
( len b1 = len p & ( for i being Nat st i in dom p holds
b1 . i = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i))) ) )
uniqueness
for b1, b2 being FinSequence of bool X st len b1 = len p & ( for i being Nat st i in dom p holds
b1 . i = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i))) ) & len b2 = len p & ( for i being Nat st i in dom p holds
b2 . i = IFEQ ((q . i),TRUE,(p . i),(X \ (p . i))) ) holds
b1 = b2
end;
theorem
for
X being
set 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 ) )