begin
:: deftheorem Def1 defines id MSUALG_3:def 1 :
for I being set
for A being ManySortedSet of I
for b3 being ManySortedFunction of A,A holds
( b3 = id A iff for i being set st i in I holds
b3 . i = id (A . i) );
:: deftheorem Def2 defines "1-1" MSUALG_3:def 2 :
for IT being Function holds
( IT is "1-1" iff for i being set
for f being Function st i in dom IT & IT . i = f holds
f is one-to-one );
theorem Th1:
:: deftheorem Def3 defines "onto" MSUALG_3:def 3 :
for I being set
for A, B being ManySortedSet of I
for IT being ManySortedFunction of A,B holds
( IT is "onto" iff for i being set st i in I holds
rng (IT . i) = B . i );
theorem Th2:
theorem
theorem Th4:
:: deftheorem MSUALG_3:def 4 :
canceled;
:: deftheorem Def5 defines "" MSUALG_3:def 5 :
for I being set
for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" holds
for b5 being ManySortedFunction of B,A holds
( b5 = F "" iff for i being set st i in I holds
b5 . i = (F . i) " );
theorem Th5:
begin
theorem Th6:
:: deftheorem MSUALG_3:def 6 :
canceled;
:: deftheorem Def7 defines # MSUALG_3:def 7 :
for S being non empty non void ManySortedSign
for U1, U2 being MSAlgebra of S
for o being OperSymbol of S
for F being ManySortedFunction of U1,U2
for x being Element of Args (o,U1) st Args (o,U1) <> {} & Args (o,U2) <> {} holds
F # x = (Frege (F * (the_arity_of o))) . x;
Lm1:
now
let S be non
empty non
void ManySortedSign ;
for U1, U2 being MSAlgebra of S
for o being OperSymbol of S
for F being ManySortedFunction of U1,U2
for x being Element of Args (o,U1)
for f, u being Function st x = f & x in Args (o,U1) & u in Args (o,U2) holds
( ( u = F # x implies for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) )let U1,
U2 be
MSAlgebra of
S;
for o being OperSymbol of S
for F being ManySortedFunction of U1,U2
for x being Element of Args (o,U1)
for f, u being Function st x = f & x in Args (o,U1) & u in Args (o,U2) holds
( ( u = F # x implies for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) )let o be
OperSymbol of
S;
for F being ManySortedFunction of U1,U2
for x being Element of Args (o,U1)
for f, u being Function st x = f & x in Args (o,U1) & u in Args (o,U2) holds
( ( u = F # x implies for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) )let F be
ManySortedFunction of
U1,
U2;
for x being Element of Args (o,U1)
for f, u being Function st x = f & x in Args (o,U1) & u in Args (o,U2) holds
( ( u = F # x implies for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) )let x be
Element of
Args (
o,
U1);
for f, u being Function st x = f & x in Args (o,U1) & u in Args (o,U2) holds
( ( u = F # x implies for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) )let f,
u be
Function;
( x = f & x in Args (o,U1) & u in Args (o,U2) implies ( ( u = F # x implies for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) ) )assume that A1:
x = f
and A2:
x in Args (
o,
U1)
and A3:
u in Args (
o,
U2)
;
( ( u = F # x implies for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) & ( ( for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x ) )A4:
rng (the_arity_of o) c= the
carrier of
S
by FINSEQ_1:def 4;
then A5:
rng (the_arity_of o) c= dom the
Sorts of
U1
by PARTFUN1:def 4;
A6:
F # x = (Frege (F * (the_arity_of o))) . x
by A2, A3, Def7;
A7:
dom ( the Sorts of U1 * (the_arity_of o)) = (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o))))
A12:
Args (
o,
U2)
= product ( the Sorts of U2 * (the_arity_of o))
by PRALG_2:10;
then A13:
dom u = dom ( the Sorts of U2 * (the_arity_of o))
by A3, CARD_3:18;
A14:
Args (
o,
U1)
= product ( the Sorts of U1 * (the_arity_of o))
by PRALG_2:10;
then A15:
dom f =
dom ( the Sorts of U1 * (the_arity_of o))
by A1, A2, CARD_3:18
.=
dom (the_arity_of o)
by A5, RELAT_1:46
;
rng (the_arity_of o) c= dom the
Sorts of
U2
by A4, PARTFUN1:def 4;
then A16:
dom u = dom (the_arity_of o)
by A13, RELAT_1:46;
now
let e be
set ;
( e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) implies ( the Sorts of U1 * (the_arity_of o)) . e = proj1 ((F * (the_arity_of o)) . e) )assume
e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o))))
;
( the Sorts of U1 * (the_arity_of o)) . e = proj1 ((F * (the_arity_of o)) . e)then
e in dom (F * (the_arity_of o))
by FUNCT_6:28;
then A17:
e in dom (the_arity_of o)
by FUNCT_1:21;
then reconsider Foe =
F . ((the_arity_of o) . e) as
Function of
( the Sorts of U1 . ((the_arity_of o) . e)),
( the Sorts of U2 . ((the_arity_of o) . e)) by FINSEQ_2:13, PBOOLE:def 18;
( the Sorts of U2 * (the_arity_of o)) . e in rng ( the Sorts of U2 * (the_arity_of o))
by A13, A16, A17, FUNCT_1:def 5;
then A18:
( the Sorts of U2 * (the_arity_of o)) . e <> {}
by A3, A12, CARD_3:37;
(
( the Sorts of U1 * (the_arity_of o)) . e = the
Sorts of
U1 . ((the_arity_of o) . e) &
( the Sorts of U2 * (the_arity_of o)) . e = the
Sorts of
U2 . ((the_arity_of o) . e) )
by A17, FUNCT_1:23;
hence ( the Sorts of U1 * (the_arity_of o)) . e =
dom Foe
by A18, FUNCT_2:def 1
.=
proj1 Foe
.=
proj1 ((F * (the_arity_of o)) . e)
by A17, FUNCT_1:23
;
verum
end;
then A19:
the
Sorts of
U1 * (the_arity_of o) = doms (F * (the_arity_of o))
by A7, FUNCT_6:def 2;
hereby ( ( for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) implies u = F # x )
assume
u = F # x
;
for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n)then A20:
u = (Frege (F * (the_arity_of o))) . x
by A2, A3, Def7;
let n be
Nat;
( n in dom f implies u . n = (F . ((the_arity_of o) /. n)) . (f . n) )assume A21:
n in dom f
;
u . n = (F . ((the_arity_of o) /. n)) . (f . n)then
(the_arity_of o) . n in the
carrier of
S
by A15, FINSEQ_2:13;
then
(the_arity_of o) . n in dom F
by PARTFUN1:def 4;
then A22:
n in dom (F * (the_arity_of o))
by A15, A21, FUNCT_1:21;
then A23:
(F * (the_arity_of o)) . n =
F . ((the_arity_of o) . n)
by FUNCT_1:22
.=
F . ((the_arity_of o) /. n)
by A15, A21, PARTFUN1:def 8
;
thus u . n =
((F * (the_arity_of o)) .. f) . n
by A1, A2, A14, A19, A20, PRALG_2:def 8
.=
(F . ((the_arity_of o) /. n)) . (f . n)
by A22, A23, PRALG_1:def 17
;
verum
end;
F # x is
Element of
product ( the Sorts of U2 * (the_arity_of o))
by PRALG_2:10;
then reconsider g =
F # x as
Function ;
A24:
rng (the_arity_of o) c= dom F
by A4, PARTFUN1:def 4;
assume A25:
for
n being
Nat st
n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n)
;
u = F # x
A26:
now
let e be
set ;
( e in dom f implies u . e = g . e )assume A27:
e in dom f
;
u . e = g . ethen reconsider n =
e as
Nat by A15;
(the_arity_of o) . n in the
carrier of
S
by A15, A27, FINSEQ_2:13;
then
(the_arity_of o) . n in dom F
by PARTFUN1:def 4;
then A28:
n in dom (F * (the_arity_of o))
by A15, A27, FUNCT_1:21;
then A29:
(F * (the_arity_of o)) . n =
F . ((the_arity_of o) . n)
by FUNCT_1:22
.=
F . ((the_arity_of o) /. n)
by A15, A27, PARTFUN1:def 8
;
thus u . e =
(F . ((the_arity_of o) /. n)) . (f . n)
by A25, A27
.=
((F * (the_arity_of o)) .. f) . n
by A28, A29, PRALG_1:def 17
.=
g . e
by A1, A2, A14, A19, A6, PRALG_2:def 8
;
verum
end;
F # x = (F * (the_arity_of o)) .. f
by A1, A2, A14, A19, A6, PRALG_2:def 8;
then dom g =
dom (F * (the_arity_of o))
by PRALG_1:def 17
.=
dom f
by A15, A24, RELAT_1:46
;
hence
u = F # x
by A15, A16, A26, FUNCT_1:9;
verum
end;
:: deftheorem Def8 defines # MSUALG_3:def 8 :
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra of S
for o being OperSymbol of S
for F being ManySortedFunction of U1,U2
for x being Element of Args (o,U1)
for b7 being Element of Args (o,U2) holds
( b7 = F # x iff for n being Nat st n in dom x holds
b7 . n = (F . ((the_arity_of o) /. n)) . (x . n) );
theorem Th7:
theorem Th8:
:: deftheorem Def9 defines is_homomorphism MSUALG_3:def 9 :
for S being non empty non void ManySortedSign
for U1, U2 being MSAlgebra of S
for F being ManySortedFunction of U1,U2 holds
( F is_homomorphism U1,U2 iff for o being OperSymbol of S st Args (o,U1) <> {} holds
for x being Element of Args (o,U1) holds (F . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U2)) . (F # x) );
theorem Th9:
theorem Th10:
:: deftheorem Def10 defines is_epimorphism MSUALG_3:def 10 :
for S being non empty non void ManySortedSign
for U1, U2 being MSAlgebra of S
for F being ManySortedFunction of U1,U2 holds
( F is_epimorphism U1,U2 iff ( F is_homomorphism U1,U2 & F is "onto" ) );
theorem Th11:
:: deftheorem Def11 defines is_monomorphism MSUALG_3:def 11 :
for S being non empty non void ManySortedSign
for U1, U2 being MSAlgebra of S
for F being ManySortedFunction of U1,U2 holds
( F is_monomorphism U1,U2 iff ( F is_homomorphism U1,U2 & F is "1-1" ) );
theorem Th12:
:: deftheorem Def12 defines is_isomorphism MSUALG_3:def 12 :
for S being non empty non void ManySortedSign
for U1, U2 being MSAlgebra of S
for F being ManySortedFunction of U1,U2 holds
( F is_isomorphism U1,U2 iff ( F is_epimorphism U1,U2 & F is_monomorphism U1,U2 ) );
theorem Th13:
Lm2:
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra of S
for H being ManySortedFunction of U1,U2 st H is_isomorphism U1,U2 holds
H "" is_homomorphism U2,U1
theorem Th14:
theorem Th15:
:: deftheorem Def13 defines are_isomorphic MSUALG_3:def 13 :
for S being non empty non void ManySortedSign
for U1, U2 being MSAlgebra of S holds
( U1,U2 are_isomorphic iff ex F being ManySortedFunction of U1,U2 st F is_isomorphism U1,U2 );
theorem Th16:
theorem
theorem
:: deftheorem Def14 defines Image MSUALG_3:def 14 :
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
for b5 being strict non-empty MSSubAlgebra of U2 holds
( b5 = Image F iff the Sorts of b5 = F .:.: the Sorts of U1 );
theorem
Lm3:
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
F is ManySortedFunction of U1,(Image F)
theorem Th20:
theorem
Lm4:
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra of S
for U3 being non-empty MSSubAlgebra of U2
for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U1,U3 st F = G & G is_homomorphism U1,U3 holds
F is_homomorphism U1,U2
theorem Th22:
theorem
theorem