begin
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;
begin
begin
:: Trivial Algebra
::