environ
vocabularies HIDDEN, FUNCT_1, FUNCT_3, PARTFUN1, RELAT_1, ZFMISC_1, XBOOLE_0, TARSKI, SUBSET_1, BINOP_1, MCART_1, FUNCOP_1, WELLORD1, MSUALG_4, FUNCT_2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, MCART_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_3, BINOP_1, WELLORD1;
definitions TARSKI, RELAT_1, FUNCT_1, WELLORD1, PARTFUN1;
theorems ZFMISC_1, RELAT_1, RELSET_1, FUNCT_1, FUNCT_2, FUNCT_3, TARSKI, MCART_1, XBOOLE_0, XBOOLE_1, GRFUNC_1, XTUPLE_0;
schemes FUNCT_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, RELSET_1, FUNCT_3;
constructors HIDDEN, PARTFUN1, BINOP_1, FUNCT_3, RELSET_1, WELLORD1, XTUPLE_0;
requirements HIDDEN, SUBSET, BOOLE;
equalities BINOP_1;
expansions TARSKI, RELAT_1, BINOP_1, FUNCT_1;
definition
let f be
Function;
existence
ex b1 being Function st
( dom b1 = dom f & ( for x being object st x in dom f holds
( ( for y, z being object st f . x = [y,z] holds
b1 . x = [z,y] ) & ( f . x = b1 . x or ex y, z being object st f . x = [y,z] ) ) ) )
uniqueness
for b1, b2 being Function st dom b1 = dom f & ( for x being object st x in dom f holds
( ( for y, z being object st f . x = [y,z] holds
b1 . x = [z,y] ) & ( f . x = b1 . x or ex y, z being object st f . x = [y,z] ) ) ) & dom b2 = dom f & ( for x being object st x in dom f holds
( ( for y, z being object st f . x = [y,z] holds
b2 . x = [z,y] ) & ( f . x = b2 . x or ex y, z being object st f . x = [y,z] ) ) ) holds
b1 = b2
involutiveness
for b1, b2 being Function st dom b1 = dom b2 & ( for x being object st x in dom b2 holds
( ( for y, z being object st b2 . x = [y,z] holds
b1 . x = [z,y] ) & ( b2 . x = b1 . x or ex y, z being object st b2 . x = [y,z] ) ) ) holds
( dom b2 = dom b1 & ( for x being object st x in dom b1 holds
( ( for y, z being object st b1 . x = [y,z] holds
b2 . x = [z,y] ) & ( b1 . x = b2 . x or ex y, z being object st b1 . x = [y,z] ) ) ) )
end;
Lm1:
for f, g, F being Function
for x being object st x in dom (F * <:f,g:>) holds
(F * <:f,g:>) . x = F . ((f . x),(g . x))
Lm2:
for o, m, r being object holds (o,m) :-> r is Function of [:{o},{m}:],{r}