environ
vocabularies HIDDEN, INT_1, ABIAN, ARYTM_1, ZFMISC_1, FUNCT_1, RELAT_1, TARSKI, FUNCOP_1, FUNCT_2, FUNCT_6, XBOOLE_0, PBOOLE, SUBSET_1, NUMBERS, NAT_1, HILBERT1, CARD_1, FUNCT_3, CARD_3, MCART_1, PARTFUN1, FINSEQ_4, XBOOLEAN, QC_LANG1, HILBERT2, FUNCT_5, ARYTM_3, FUNCT_4, XXREAL_0, HILBERT3, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, INT_1, RELAT_1, FUNCT_1, PBOOLE, CARD_1, CARD_3, ABIAN, PARTFUN1, FUNCT_2, BINOP_1, XXREAL_0, FUNCT_3, FUNCOP_1, FUNCT_4, FUNCT_5, FUNCT_6, PRALG_1, PRALG_2, MSUALG_3, HILBERT1, HILBERT2;
definitions PBOOLE, FUNCT_1, FUNCT_2, TARSKI, HILBERT1, ABIAN, FUNCOP_1, XBOOLE_0;
theorems PBOOLE, ZFMISC_1, MSUALG_3, FUNCT_2, RELAT_1, RELSET_1, FUNCT_1, FUNCT_3, TARSKI, FUNCOP_1, PARTFUN2, PRALG_2, CARD_3, FUNCT_6, MSSUBFAM, FUNCT_5, FUNCTOR0, HILBERT1, FUNCT_4, INT_1, TOPREAL6, PRALG_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_1, XXREAL_0, CARD_1, PARTFUN1, XTUPLE_0;
schemes HILBERT2, FUNCT_2;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, PARTFUN1, FUNCT_2, FUNCOP_1, FUNCT_4, NUMBERS, XREAL_0, INT_1, PBOOLE, ABIAN, HILBERT1, RELSET_1, ZFMISC_1, MSSUBFAM, CARD_1;
constructors HIDDEN, XXREAL_0, NAT_D, ABIAN, CAT_2, PRALG_1, PRALG_2, MSUALG_3, HILBERT2, RELSET_1, FUNCT_5, FUNCT_4;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET;
equalities HILBERT1, FUNCOP_1, BINOP_1, SUBSET_1, ORDINAL1, CARD_1;
expansions PBOOLE, FUNCT_1, ABIAN;
theorem Th9:
for
a,
b,
x,
y,
x9,
y9 being
set st
a <> b & (
a,
b)
--> (
x,
y)
= (
a,
b)
--> (
x9,
y9) holds
(
x = x9 &
y = y9 )
theorem Th12:
for
a,
b,
c,
d being
set st
a <> b holds
((a,b) --> (c,d)) * ((a,b) --> (b,a)) = (
a,
b)
--> (
d,
c)
definition
let A,
B be non
empty set ;
let P be
Permutation of
A;
let Q be
Function of
B,
B;
existence
ex b1 being Function of (Funcs (A,B)),(Funcs (A,B)) st
for f being Function of A,B holds b1 . f = (Q * f) * (P ")
uniqueness
for b1, b2 being Function of (Funcs (A,B)),(Funcs (A,B)) st ( for f being Function of A,B holds b1 . f = (Q * f) * (P ") ) & ( for f being Function of A,B holds b2 . f = (Q * f) * (P ") ) holds
b1 = b2
end;
definition
let V be
SetValuation;
existence
ex b1 being ManySortedSet of HP-WFF st
( b1 . VERUM = 1 & ( for n being Element of NAT holds b1 . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds
( b1 . (p '&' q) = [:(b1 . p),(b1 . q):] & b1 . (p => q) = Funcs ((b1 . p),(b1 . q)) ) ) )
uniqueness
for b1, b2 being ManySortedSet of HP-WFF st b1 . VERUM = 1 & ( for n being Element of NAT holds b1 . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds
( b1 . (p '&' q) = [:(b1 . p),(b1 . q):] & b1 . (p => q) = Funcs ((b1 . p),(b1 . q)) ) ) & b2 . VERUM = 1 & ( for n being Element of NAT holds b2 . (prop n) = V . n ) & ( for p, q being Element of HP-WFF holds
( b2 . (p '&' q) = [:(b2 . p),(b2 . q):] & b2 . (p => q) = Funcs ((b2 . p),(b2 . q)) ) ) holds
b1 = b2
end;
definition
let V be
SetValuation;
let P be
Permutation of
V;
existence
ex b1 being ManySortedFunction of SetVal V, SetVal V st
( b1 . VERUM = id 1 & ( for n being Element of NAT holds b1 . (prop n) = P . n ) & ( for p, q being Element of HP-WFF ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st
( p9 = b1 . p & q9 = b1 . q & b1 . (p '&' q) = [:p9,q9:] & b1 . (p => q) = p9 => q9 ) ) )
uniqueness
for b1, b2 being ManySortedFunction of SetVal V, SetVal V st b1 . VERUM = id 1 & ( for n being Element of NAT holds b1 . (prop n) = P . n ) & ( for p, q being Element of HP-WFF ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st
( p9 = b1 . p & q9 = b1 . q & b1 . (p '&' q) = [:p9,q9:] & b1 . (p => q) = p9 => q9 ) ) & b2 . VERUM = id 1 & ( for n being Element of NAT holds b2 . (prop n) = P . n ) & ( for p, q being Element of HP-WFF ex p9 being Permutation of (SetVal (V,p)) ex q9 being Permutation of (SetVal (V,q)) st
( p9 = b2 . p & q9 = b2 . q & b2 . (p '&' q) = [:p9,q9:] & b2 . (p => q) = p9 => q9 ) ) holds
b1 = b2
end;