environ
vocabularies HIDDEN, UNIALG_1, NAT_1, XBOOLE_0, FINSEQ_1, ZFMISC_1, MCART_1, RELAT_1, FUNCT_1, FUNCT_2, PARTFUN1, FINSEQ_2, SUBSET_1, TARSKI, NUMBERS, STRUCT_0, CQC_SIM1, UNIALG_2, PBOOLE, FUNCOP_1, RLVECT_2, CARD_3, CARD_1, FINSEQ_4, FUNCT_5, PRALG_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, NUMBERS, NAT_1, STRUCT_0, RELAT_1, FUNCT_1, FINSEQ_1, FUNCT_2, BINOP_1, FUNCOP_1, MCART_1, DOMAIN_1, PARTFUN1, FINSEQ_2, FUNCT_4, FUNCT_5, CARD_3, MARGREL1, DTCONSTR, UNIALG_1, UNIALG_2, PBOOLE;
definitions TARSKI, UNIALG_2, FUNCT_1, PBOOLE, XBOOLE_0, MARGREL1;
theorems TARSKI, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_2, FUNCOP_1, UNIALG_1, DOMAIN_1, ZFMISC_1, MCART_1, UNIALG_2, FUNCT_2, FUNCT_5, CARD_3, FUNCT_4, FINSEQ_3, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, MARGREL1, CARD_1, XTUPLE_0;
schemes FINSEQ_1, PARTFUN1, FUNCT_2, FUNCT_1, CLASSES1;
registrations SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, PARTFUN1, FUNCOP_1, FINSEQ_1, FINSEQ_2, CARD_3, PBOOLE, STRUCT_0, UNIALG_1, CARD_1, RELSET_1, MARGREL1, XTUPLE_0;
constructors HIDDEN, BINOP_1, DOMAIN_1, FUNCT_4, FUNCT_5, CARD_3, PBOOLE, UNIALG_2, DTCONSTR, STRUCT_0, RELSET_1, XTUPLE_0, NUMBERS;
requirements HIDDEN, BOOLE, SUBSET;
equalities UNIALG_2, XBOOLE_0, BINOP_1, FINSEQ_2, FUNCOP_1, ORDINAL1;
expansions TARSKI, UNIALG_2, FUNCT_1, PBOOLE, MARGREL1;
definition
let A,
B be non
empty set ;
let f1 be non
empty homogeneous quasi_total PartFunc of
(A *),
A;
let f2 be non
empty homogeneous quasi_total PartFunc of
(B *),
B;
assume A1:
arity f1 = arity f2
;
existence
ex b1 being non empty homogeneous quasi_total PartFunc of ([:A,B:] *),[:A,B:] st
( dom b1 = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom b1 holds
b1 . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) )
uniqueness
for b1, b2 being non empty homogeneous quasi_total PartFunc of ([:A,B:] *),[:A,B:] st dom b1 = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom b1 holds
b1 . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) & dom b2 = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom b2 holds
b2 . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) holds
b1 = b2
end;
::
deftheorem Def3 defines
[[: PRALG_1:def 3 :
for A, B being non empty set
for f1 being non empty homogeneous quasi_total PartFunc of (A *),A
for f2 being non empty homogeneous quasi_total PartFunc of (B *),B st arity f1 = arity f2 holds
for b5 being non empty homogeneous quasi_total PartFunc of ([:A,B:] *),[:A,B:] holds
( b5 = [[:f1,f2:]] iff ( dom b5 = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom b5 holds
b5 . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) ) );
definition
let U1,
U2 be
Universal_Algebra;
assume A1:
U1,
U2 are_similar
;
existence
ex b1 being PFuncFinSequence of [: the carrier of U1, the carrier of U2:] st
( len b1 = len the charact of U1 & ( for n being Nat st n in dom b1 holds
for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds
b1 . n = [[:h1,h2:]] ) )
uniqueness
for b1, b2 being PFuncFinSequence of [: the carrier of U1, the carrier of U2:] st len b1 = len the charact of U1 & ( for n being Nat st n in dom b1 holds
for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds
b1 . n = [[:h1,h2:]] ) & len b2 = len the charact of U1 & ( for n being Nat st n in dom b2 holds
for h1 being non empty homogeneous quasi_total PartFunc of ( the carrier of U1 *), the carrier of U1
for h2 being non empty homogeneous quasi_total PartFunc of ( the carrier of U2 *), the carrier of U2 st h1 = the charact of U1 . n & h2 = the charact of U2 . n holds
b2 . n = [[:h1,h2:]] ) holds
b1 = b2
end;
definition
let A,
B be non
empty set ;
existence
ex b1 being Function of [:A,B:],[:B,A:] st
for a being Element of [:A,B:] holds b1 . a = [(a `2),(a `1)]
uniqueness
for b1, b2 being Function of [:A,B:],[:B,A:] st ( for a being Element of [:A,B:] holds b1 . a = [(a `2),(a `1)] ) & ( for a being Element of [:A,B:] holds b2 . a = [(a `2),(a `1)] ) holds
b1 = b2
end;
:: Trivial Algebra
::