environ
vocabularies HIDDEN, NUMBERS, NAT_1, XBOOLE_0, SUBSET_1, FINSEQ_2, FINSEQ_1, ORDINAL4, PARTFUN1, RELAT_1, ARYTM_3, CARD_1, MARGREL1, XBOOLEAN, XCMPLX_0, FUNCT_1, XXREAL_0, ARYTM_1, FUNCOP_1, POWER, BINOP_2, SETWISEO, REAL_1, BINARITH;
notations HIDDEN, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, XBOOLEAN, MARGREL1, FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1, BINOP_2, SETWISEO, FUNCOP_1, SETWOP_2, SERIES_1, FINSEQ_1, FINSEQ_2, XXREAL_0, NAT_1, NAT_D, TREES_3;
definitions FINSEQ_1, TARSKI;
theorems NAT_1, INT_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, FUNCT_1, TARSKI, POWER, FINSOP_1, XBOOLE_0, BINOP_2, XREAL_1, XXREAL_0, XBOOLEAN, FUNCOP_1, PARTFUN1, FINSEQ_3, XREAL_0, NAT_D, CARD_1;
schemes FINSEQ_1, FINSEQ_2, NAT_1;
registrations ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, BINOP_2, XBOOLEAN, MARGREL1, FINSEQ_2, CARD_1;
constructors HIDDEN, BINOP_1, SETWISEO, XXREAL_0, NAT_1, INT_1, BINOP_2, MARGREL1, PARTFUN1, FINSOP_1, SERIES_1, RFINSEQ, REAL_1, NAT_D, RELSET_1, FINSEQ_2, TREES_3, FUNCOP_1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities FINSEQ_1, XBOOLEAN;
expansions ;
definition
let n be
Nat;
let x be
Tuple of
n,
BOOLEAN ;
existence
ex b1 being Tuple of n, NAT st
for i being Nat st i in Seg n holds
b1 /. i = IFEQ ((x /. i),FALSE,0,(2 to_power (i -' 1)))
uniqueness
for b1, b2 being Tuple of n, NAT st ( for i being Nat st i in Seg n holds
b1 /. i = IFEQ ((x /. i),FALSE,0,(2 to_power (i -' 1))) ) & ( for i being Nat st i in Seg n holds
b2 /. i = IFEQ ((x /. i),FALSE,0,(2 to_power (i -' 1))) ) holds
b1 = b2
end;