:: MSUALG_3 semantic presentation
begin
definition
let I be non empty set ;
let A, B be ManySortedSet of I;
let F be ManySortedFunction of A,B;
let i be Element of I;
:: original: .
redefine funcF . i -> Function of (A . i),(B . i);
coherence
F . i is Function of (A . i),(B . i) by PBOOLE:def_15;
end;
definition
let S be non empty ManySortedSign ;
let U1, U2 be MSAlgebra over S;
mode ManySortedFunction of U1,U2 is ManySortedFunction of the Sorts of U1, the Sorts of U2;
end;
definition
let I be set ;
let A be ManySortedSet of I;
func id A -> ManySortedFunction of A,A means :Def1: :: MSUALG_3:def 1
for i being set st i in I holds
it . i = id (A . i);
existence
ex b1 being ManySortedFunction of A,A st
for i being set st i in I holds
b1 . i = id (A . i)
proof
deffunc H1( set ) -> Element of K19(K20((A . $1),(A . $1))) = id (A . $1);
consider f being Function such that
A1: ( dom f = I & ( for i being set st i in I holds
f . i = H1(i) ) ) from FUNCT_1:sch_3();
reconsider f = f as ManySortedSet of I by A1, PARTFUN1:def_2, RELAT_1:def_18;
for x being set st x in dom f holds
f . x is Function
proof
let x be set ; ::_thesis: ( x in dom f implies f . x is Function )
assume x in dom f ; ::_thesis: f . x is Function
then f . x = id (A . x) by A1;
hence f . x is Function ; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of I by FUNCOP_1:def_6;
for i being set st i in I holds
f . i is Function of (A . i),(A . i)
proof
let i be set ; ::_thesis: ( i in I implies f . i is Function of (A . i),(A . i) )
assume i in I ; ::_thesis: f . i is Function of (A . i),(A . i)
then f . i = id (A . i) by A1;
hence f . i is Function of (A . i),(A . i) ; ::_thesis: verum
end;
then reconsider f = f as ManySortedFunction of A,A by PBOOLE:def_15;
take f ; ::_thesis: for i being set st i in I holds
f . i = id (A . i)
thus for i being set st i in I holds
f . i = id (A . i) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being ManySortedFunction of A,A st ( for i being set st i in I holds
b1 . i = id (A . i) ) & ( for i being set st i in I holds
b2 . i = id (A . i) ) holds
b1 = b2
proof
let F, G be ManySortedFunction of A,A; ::_thesis: ( ( for i being set st i in I holds
F . i = id (A . i) ) & ( for i being set st i in I holds
G . i = id (A . i) ) implies F = G )
assume that
A2: for i being set st i in I holds
F . i = id (A . i) and
A3: for i being set st i in I holds
G . i = id (A . i) ; ::_thesis: F = G
A4: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
F_._i_=_G_._i
let i be set ; ::_thesis: ( i in I implies F . i = G . i )
assume A5: i in I ; ::_thesis: F . i = G . i
then F . i = id (A . i) by A2;
hence F . i = G . i by A3, A5; ::_thesis: verum
end;
( dom F = I & dom G = I ) by PARTFUN1:def_2;
hence F = G by A4, FUNCT_1:2; ::_thesis: verum
end;
end;
:: 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) );
definition
let IT be Function;
attrIT is "1-1" means :Def2: :: MSUALG_3:def 2
for i being set
for f being Function st i in dom IT & IT . i = f holds
f is one-to-one ;
end;
:: 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 );
registration
let I be set ;
cluster Relation-like I -defined Function-like total V41() V42() "1-1" for set ;
existence
ex b1 being ManySortedFunction of I st b1 is "1-1"
proof
set A = the ManySortedSet of I;
take F = id the ManySortedSet of I; ::_thesis: F is "1-1"
let i be set ; :: according to MSUALG_3:def_2 ::_thesis: for f being Function st i in dom F & F . i = f holds
f is one-to-one
let f be Function; ::_thesis: ( i in dom F & F . i = f implies f is one-to-one )
A1: dom (id the ManySortedSet of I) = I by PARTFUN1:def_2;
assume ( i in dom F & F . i = f ) ; ::_thesis: f is one-to-one
then f = id ( the ManySortedSet of I . i) by A1, Def1;
hence f is one-to-one ; ::_thesis: verum
end;
end;
theorem Th1: :: MSUALG_3:1
for I being set
for F being ManySortedFunction of I holds
( F is "1-1" iff for i being set st i in I holds
F . i is one-to-one )
proof
let I be set ; ::_thesis: for F being ManySortedFunction of I holds
( F is "1-1" iff for i being set st i in I holds
F . i is one-to-one )
let F be ManySortedFunction of I; ::_thesis: ( F is "1-1" iff for i being set st i in I holds
F . i is one-to-one )
A1: dom F = I by PARTFUN1:def_2;
hence ( F is "1-1" implies for i being set st i in I holds
F . i is one-to-one ) by Def2; ::_thesis: ( ( for i being set st i in I holds
F . i is one-to-one ) implies F is "1-1" )
assume for i being set st i in I holds
F . i is one-to-one ; ::_thesis: F is "1-1"
then for i being set
for f being Function st i in dom F & f = F . i holds
f is one-to-one by A1;
hence F is "1-1" by Def2; ::_thesis: verum
end;
definition
let I be set ;
let A, B be ManySortedSet of I;
let IT be ManySortedFunction of A,B;
attrIT is "onto" means :Def3: :: MSUALG_3:def 3
for i being set st i in I holds
rng (IT . i) = B . i;
end;
:: 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: :: MSUALG_3:2
for I being set
for A, B, C being ManySortedSet of I
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C holds
( dom (G ** F) = I & ( for i being set st i in I holds
(G ** F) . i = (G . i) * (F . i) ) )
proof
let I be set ; ::_thesis: for A, B, C being ManySortedSet of I
for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C holds
( dom (G ** F) = I & ( for i being set st i in I holds
(G ** F) . i = (G . i) * (F . i) ) )
let A, B, C be ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B
for G being ManySortedFunction of B,C holds
( dom (G ** F) = I & ( for i being set st i in I holds
(G ** F) . i = (G . i) * (F . i) ) )
let F be ManySortedFunction of A,B; ::_thesis: for G being ManySortedFunction of B,C holds
( dom (G ** F) = I & ( for i being set st i in I holds
(G ** F) . i = (G . i) * (F . i) ) )
let G be ManySortedFunction of B,C; ::_thesis: ( dom (G ** F) = I & ( for i being set st i in I holds
(G ** F) . i = (G . i) * (F . i) ) )
( dom F = I & dom G = I ) by PARTFUN1:def_2;
then (dom F) /\ (dom G) = I ;
hence A1: dom (G ** F) = I by PBOOLE:def_19; ::_thesis: for i being set st i in I holds
(G ** F) . i = (G . i) * (F . i)
let i be set ; ::_thesis: ( i in I implies (G ** F) . i = (G . i) * (F . i) )
thus ( i in I implies (G ** F) . i = (G . i) * (F . i) ) by A1, PBOOLE:def_19; ::_thesis: verum
end;
definition
let I be set ;
let A be ManySortedSet of I;
let B, C be V2() ManySortedSet of I;
let F be ManySortedFunction of A,B;
let G be ManySortedFunction of B,C;
:: original: **
redefine funcG ** F -> ManySortedFunction of A,C;
coherence
G ** F is ManySortedFunction of A,C
proof
dom (G ** F) = I by Th2;
then reconsider fg = G ** F as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
reconsider fg = fg as ManySortedFunction of I ;
for i being set st i in I holds
fg . i is Function of (A . i),(C . i)
proof
let i be set ; ::_thesis: ( i in I implies fg . i is Function of (A . i),(C . i) )
assume A1: i in I ; ::_thesis: fg . i is Function of (A . i),(C . i)
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15;
reconsider g = G . i as Function of (B . i),(C . i) by A1, PBOOLE:def_15;
(G ** F) . i = g * f by A1, Th2;
hence fg . i is Function of (A . i),(C . i) by A1; ::_thesis: verum
end;
hence G ** F is ManySortedFunction of A,C by PBOOLE:def_15; ::_thesis: verum
end;
end;
theorem :: MSUALG_3:3
for I being set
for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B holds F ** (id A) = F
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B holds F ** (id A) = F
let A, B be ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B holds F ** (id A) = F
let F be ManySortedFunction of A,B; ::_thesis: F ** (id A) = F
dom (F ** (id A)) = (dom F) /\ (dom (id A)) by PBOOLE:def_19
.= I /\ (dom (id A)) by PARTFUN1:def_2
.= I /\ I by PARTFUN1:def_2
.= I ;
then reconsider G = F ** (id A) as ManySortedFunction of I by PARTFUN1:def_2, RELAT_1:def_18;
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
G_._i_=_F_._i
let i be set ; ::_thesis: ( i in I implies G . b1 = F . b1 )
assume A1: i in I ; ::_thesis: G . b1 = F . b1
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15;
reconsider g = (id A) . i as Function of (A . i),(A . i) by A1, PBOOLE:def_15;
A2: G . i = f * g by A1, Th2
.= f * (id (A . i)) by A1, Def1 ;
percases not ( B . i = {} & not A . i = {} & not ( B . i = {} & A . i <> {} ) ) ;
suppose ( B . i = {} implies A . i = {} ) ; ::_thesis: G . b1 = F . b1
then dom f = A . i by FUNCT_2:def_1;
hence G . i = F . i by A2, RELAT_1:52; ::_thesis: verum
end;
suppose ( B . i = {} & A . i <> {} ) ; ::_thesis: G . b1 = F . b1
then f = {} ;
hence G . i = F . i by A2; ::_thesis: verum
end;
end;
end;
hence F ** (id A) = F by PBOOLE:3; ::_thesis: verum
end;
theorem Th4: :: MSUALG_3:4
for I being set
for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B holds (id B) ** F = F
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B holds (id B) ** F = F
let A, B be ManySortedSet of I; ::_thesis: for F being ManySortedFunction of A,B holds (id B) ** F = F
let F be ManySortedFunction of A,B; ::_thesis: (id B) ** F = F
dom ((id B) ** F) = (dom (id B)) /\ (dom F) by PBOOLE:def_19
.= I /\ (dom F) by PARTFUN1:def_2
.= I /\ I by PARTFUN1:def_2
.= I ;
then reconsider G = (id B) ** F as ManySortedFunction of I by PARTFUN1:def_2, RELAT_1:def_18;
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
G_._i_=_F_._i
let i be set ; ::_thesis: ( i in I implies G . i = F . i )
assume A1: i in I ; ::_thesis: G . i = F . i
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15;
reconsider g = (id B) . i as Function of (B . i),(B . i) by A1, PBOOLE:def_15;
( g = id (B . i) & G . i = g * f ) by A1, Def1, Th2;
hence G . i = F . i by FUNCT_2:17; ::_thesis: verum
end;
hence (id B) ** F = F by PBOOLE:3; ::_thesis: verum
end;
definition
let I be set ;
let A, B be ManySortedSet of I;
let F be ManySortedFunction of A,B;
assume that
A1: F is "1-1" and
A2: F is "onto" ;
funcF "" -> ManySortedFunction of B,A means :Def4: :: MSUALG_3:def 4
for i being set st i in I holds
it . i = (F . i) " ;
existence
ex b1 being ManySortedFunction of B,A st
for i being set st i in I holds
b1 . i = (F . i) "
proof
defpred S1[ set , set ] means $2 = (F . $1) " ;
A3: for i being set st i in I holds
ex u being set st S1[i,u] ;
consider H being Function such that
A4: ( dom H = I & ( for i being set st i in I holds
S1[i,H . i] ) ) from CLASSES1:sch_1(A3);
reconsider H = H as ManySortedSet of I by A4, PARTFUN1:def_2, RELAT_1:def_18;
for x being set st x in dom H holds
H . x is Function
proof
let x be set ; ::_thesis: ( x in dom H implies H . x is Function )
assume A5: x in dom H ; ::_thesis: H . x is Function
then x in I by PARTFUN1:def_2;
then reconsider f = F . x as Function of (A . x),(B . x) by PBOOLE:def_15;
H . x = f " by A4, A5;
hence H . x is Function ; ::_thesis: verum
end;
then reconsider H = H as ManySortedFunction of I by FUNCOP_1:def_6;
for i being set st i in I holds
H . i is Function of (B . i),(A . i)
proof
let i be set ; ::_thesis: ( i in I implies H . i is Function of (B . i),(A . i) )
assume A6: i in I ; ::_thesis: H . i is Function of (B . i),(A . i)
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15;
i in dom F by A6, PARTFUN1:def_2;
then A7: f is one-to-one by A1, Def2;
rng f = B . i by A2, A6, Def3;
then f " is Function of (B . i),(A . i) by A7, FUNCT_2:25;
hence H . i is Function of (B . i),(A . i) by A4, A6; ::_thesis: verum
end;
then reconsider H = H as ManySortedFunction of B,A by PBOOLE:def_15;
take H ; ::_thesis: for i being set st i in I holds
H . i = (F . i) "
thus for i being set st i in I holds
H . i = (F . i) " by A4; ::_thesis: verum
end;
uniqueness
for b1, b2 being ManySortedFunction of B,A st ( for i being set st i in I holds
b1 . i = (F . i) " ) & ( for i being set st i in I holds
b2 . i = (F . i) " ) holds
b1 = b2
proof
let H1, H2 be ManySortedFunction of B,A; ::_thesis: ( ( for i being set st i in I holds
H1 . i = (F . i) " ) & ( for i being set st i in I holds
H2 . i = (F . i) " ) implies H1 = H2 )
assume that
A8: for i being set st i in I holds
H1 . i = (F . i) " and
A9: for i being set st i in I holds
H2 . i = (F . i) " ; ::_thesis: H1 = H2
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
H1_._i_=_H2_._i
let i be set ; ::_thesis: ( i in I implies H1 . i = H2 . i )
assume A10: i in I ; ::_thesis: H1 . i = H2 . i
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def_15;
H1 . i = f " by A8, A10;
hence H1 . i = H2 . i by A9, A10; ::_thesis: verum
end;
hence H1 = H2 by PBOOLE:3; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines "" MSUALG_3:def_4_:_
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: :: MSUALG_3:5
for I being set
for A, B being V2() ManySortedSet of I
for H being ManySortedFunction of A,B
for H1 being ManySortedFunction of B,A st H is "1-1" & H is "onto" & H1 = H "" holds
( H ** H1 = id B & H1 ** H = id A )
proof
let I be set ; ::_thesis: for A, B being V2() ManySortedSet of I
for H being ManySortedFunction of A,B
for H1 being ManySortedFunction of B,A st H is "1-1" & H is "onto" & H1 = H "" holds
( H ** H1 = id B & H1 ** H = id A )
let A, B be V2() ManySortedSet of I; ::_thesis: for H being ManySortedFunction of A,B
for H1 being ManySortedFunction of B,A st H is "1-1" & H is "onto" & H1 = H "" holds
( H ** H1 = id B & H1 ** H = id A )
let H be ManySortedFunction of A,B; ::_thesis: for H1 being ManySortedFunction of B,A st H is "1-1" & H is "onto" & H1 = H "" holds
( H ** H1 = id B & H1 ** H = id A )
let H1 be ManySortedFunction of B,A; ::_thesis: ( H is "1-1" & H is "onto" & H1 = H "" implies ( H ** H1 = id B & H1 ** H = id A ) )
assume that
A1: ( H is "1-1" & H is "onto" ) and
A2: H1 = H "" ; ::_thesis: ( H ** H1 = id B & H1 ** H = id A )
A3: now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(H_**_H1)_._i_=_id_(B_._i)
let i be set ; ::_thesis: ( i in I implies (H ** H1) . i = id (B . i) )
assume A4: i in I ; ::_thesis: (H ** H1) . i = id (B . i)
then reconsider h = H . i as Function of (A . i),(B . i) by PBOOLE:def_15;
reconsider h1 = H1 . i as Function of (B . i),(A . i) by A4, PBOOLE:def_15;
i in dom H by A4, PARTFUN1:def_2;
then A5: h is one-to-one by A1, Def2;
h1 = h " by A1, A2, A4, Def4;
then h * h1 = id (rng h) by A5, FUNCT_1:39;
then h * h1 = id (B . i) by A1, A4, Def3;
hence (H ** H1) . i = id (B . i) by A4, Th2; ::_thesis: verum
end;
for i being set st i in I holds
(H1 ** H) . i = id (A . i)
proof
let i be set ; ::_thesis: ( i in I implies (H1 ** H) . i = id (A . i) )
assume A6: i in I ; ::_thesis: (H1 ** H) . i = id (A . i)
then reconsider h = H . i as Function of (A . i),(B . i) by PBOOLE:def_15;
reconsider h1 = H1 . i as Function of (B . i),(A . i) by A6, PBOOLE:def_15;
i in dom H by A6, PARTFUN1:def_2;
then A7: h is one-to-one by A1, Def2;
( h1 = h " & dom h = A . i ) by A1, A2, A6, Def4, FUNCT_2:def_1;
then h1 * h = id (A . i) by A7, FUNCT_1:39;
hence (H1 ** H) . i = id (A . i) by A6, Th2; ::_thesis: verum
end;
hence ( H ** H1 = id B & H1 ** H = id A ) by A3, Def1; ::_thesis: verum
end;
registration
let S be non empty non void ManySortedSign ;
let U1 be non-empty MSAlgebra over S;
let o be OperSymbol of S;
cluster Args (o,U1) -> functional ;
coherence
Args (o,U1) is functional
proof
Args (o,U1) = product ( the Sorts of U1 * (the_arity_of o)) by PRALG_2:3;
hence Args (o,U1) is functional ; ::_thesis: verum
end;
end;
begin
theorem Th6: :: MSUALG_3:6
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U1 being MSAlgebra over S
for x being Function st x in Args (o,U1) holds
( dom x = dom (the_arity_of o) & ( for y being set st y in dom ( the Sorts of U1 * (the_arity_of o)) holds
x . y in ( the Sorts of U1 * (the_arity_of o)) . y ) )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for o being OperSymbol of S
for U1 being MSAlgebra over S
for x being Function st x in Args (o,U1) holds
( dom x = dom (the_arity_of o) & ( for y being set st y in dom ( the Sorts of U1 * (the_arity_of o)) holds
x . y in ( the Sorts of U1 * (the_arity_of o)) . y ) )
let o be OperSymbol of S; ::_thesis: for U1 being MSAlgebra over S
for x being Function st x in Args (o,U1) holds
( dom x = dom (the_arity_of o) & ( for y being set st y in dom ( the Sorts of U1 * (the_arity_of o)) holds
x . y in ( the Sorts of U1 * (the_arity_of o)) . y ) )
let U1 be MSAlgebra over S; ::_thesis: for x being Function st x in Args (o,U1) holds
( dom x = dom (the_arity_of o) & ( for y being set st y in dom ( the Sorts of U1 * (the_arity_of o)) holds
x . y in ( the Sorts of U1 * (the_arity_of o)) . y ) )
let x be Function; ::_thesis: ( x in Args (o,U1) implies ( dom x = dom (the_arity_of o) & ( for y being set st y in dom ( the Sorts of U1 * (the_arity_of o)) holds
x . y in ( the Sorts of U1 * (the_arity_of o)) . y ) ) )
A1: Args (o,U1) = product ( the Sorts of U1 * (the_arity_of o)) by PRALG_2:3;
dom the Sorts of U1 = the carrier of S by PARTFUN1:def_2;
then A2: rng (the_arity_of o) c= dom the Sorts of U1 by FINSEQ_1:def_4;
assume A3: x in Args (o,U1) ; ::_thesis: ( dom x = dom (the_arity_of o) & ( for y being set st y in dom ( the Sorts of U1 * (the_arity_of o)) holds
x . y in ( the Sorts of U1 * (the_arity_of o)) . y ) )
then dom x = dom ( the Sorts of U1 * (the_arity_of o)) by A1, CARD_3:9;
hence ( dom x = dom (the_arity_of o) & ( for y being set st y in dom ( the Sorts of U1 * (the_arity_of o)) holds
x . y in ( the Sorts of U1 * (the_arity_of o)) . y ) ) by A3, A1, A2, CARD_3:9, RELAT_1:27; ::_thesis: verum
end;
definition
let S be non empty non void ManySortedSign ;
let U1, U2 be MSAlgebra over S;
let o be OperSymbol of S;
let F be ManySortedFunction of U1,U2;
let x be Element of Args (o,U1);
assume that
A1: Args (o,U1) <> {} and
A2: Args (o,U2) <> {} ;
funcF # x -> Element of Args (o,U2) equals :Def5: :: MSUALG_3:def 5
(Frege (F * (the_arity_of o))) . x;
coherence
(Frege (F * (the_arity_of o))) . x is Element of Args (o,U2)
proof
A3: dom ( the Sorts of U1 * (the_arity_of o)) = (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o))))
proof
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) c= dom ( the Sorts of U1 * (the_arity_of o))
let e be set ; ::_thesis: ( e in dom ( the Sorts of U1 * (the_arity_of o)) implies e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) )
A4: (F * (the_arity_of o)) . e is Function ;
assume A5: e in dom ( the Sorts of U1 * (the_arity_of o)) ; ::_thesis: e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o))))
then (the_arity_of o) . e in dom the Sorts of U1 by FUNCT_1:11;
then (the_arity_of o) . e in the carrier of S by PARTFUN1:def_2;
then A6: (the_arity_of o) . e in dom F by PARTFUN1:def_2;
e in dom (the_arity_of o) by A5, FUNCT_1:11;
then e in dom (F * (the_arity_of o)) by A6, FUNCT_1:11;
hence e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) by A4, FUNCT_6:19; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) or e in dom ( the Sorts of U1 * (the_arity_of o)) )
assume e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) ; ::_thesis: e in dom ( the Sorts of U1 * (the_arity_of o))
then e in dom (F * (the_arity_of o)) by FUNCT_6:19;
then A7: e in dom (the_arity_of o) by FUNCT_1:11;
then reconsider f = e as Element of NAT ;
(the_arity_of o) . f in the carrier of S by A7, FINSEQ_2:11;
then (the_arity_of o) . e in dom the Sorts of U1 by PARTFUN1:def_2;
hence e in dom ( the Sorts of U1 * (the_arity_of o)) by A7, FUNCT_1:11; ::_thesis: verum
end;
now__::_thesis:_for_e_being_set_st_e_in_(F_*_(the_arity_of_o))_"_(SubFuncs_(rng_(F_*_(the_arity_of_o))))_holds_
(_the_Sorts_of_U1_*_(the_arity_of_o))_._e_=_proj1_((F_*_(the_arity_of_o))_._e)
let e be set ; ::_thesis: ( 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) )
A8: product ( the Sorts of U2 * (the_arity_of o)) <> {} by A2, PRALG_2:3;
assume e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) ; ::_thesis: ( 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:19;
then A9: e in dom (the_arity_of o) by FUNCT_1:11;
then reconsider f = e as Element of NAT ;
(the_arity_of o) . f in the carrier of S by A9, FINSEQ_2:11;
then (the_arity_of o) . e in dom the Sorts of U2 by PARTFUN1:def_2;
then A10: e in dom ( the Sorts of U2 * (the_arity_of o)) by A9, FUNCT_1:11;
A11: ( the Sorts of U2 * (the_arity_of o)) . e = the Sorts of U2 . ((the_arity_of o) . e) by A9, FUNCT_1:13;
A12: now__::_thesis:_not_the_Sorts_of_U2_._((the_arity_of_o)_._e)_=_{}
assume the Sorts of U2 . ((the_arity_of o) . e) = {} ; ::_thesis: contradiction
then {} in rng ( the Sorts of U2 * (the_arity_of o)) by A10, A11, FUNCT_1:def_3;
hence contradiction by A8, CARD_3:26; ::_thesis: verum
end;
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 A9, FINSEQ_2:11, PBOOLE:def_15;
thus ( the Sorts of U1 * (the_arity_of o)) . e = the Sorts of U1 . ((the_arity_of o) . e) by A9, FUNCT_1:13
.= dom Foe by A12, FUNCT_2:def_1
.= proj1 Foe
.= proj1 ((F * (the_arity_of o)) . e) by A9, FUNCT_1:13 ; ::_thesis: verum
end;
then A13: the Sorts of U1 * (the_arity_of o) = doms (F * (the_arity_of o)) by A3, FUNCT_6:def_2;
x in Args (o,U1) by A1;
then A14: x in product ( the Sorts of U1 * (the_arity_of o)) by PRALG_2:3;
then consider f being Function such that
A15: x = f and
dom f = dom (doms (F * (the_arity_of o))) and
A16: for e being set st e in dom (doms (F * (the_arity_of o))) holds
f . e in (doms (F * (the_arity_of o))) . e by A13, CARD_3:def_5;
A17: dom ((F * (the_arity_of o)) .. f) = dom (F * (the_arity_of o)) by PRALG_1:def_17;
A18: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def_4;
then A19: rng (the_arity_of o) c= dom the Sorts of U2 by PARTFUN1:def_2;
rng (the_arity_of o) c= dom F by A18, PARTFUN1:def_2;
then A20: dom (F * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27
.= dom ( the Sorts of U2 * (the_arity_of o)) by A19, RELAT_1:27 ;
A21: now__::_thesis:_for_e_being_set_st_e_in_dom_(_the_Sorts_of_U2_*_(the_arity_of_o))_holds_
((F_*_(the_arity_of_o))_.._f)_._e_in_(_the_Sorts_of_U2_*_(the_arity_of_o))_._e
let e be set ; ::_thesis: ( e in dom ( the Sorts of U2 * (the_arity_of o)) implies ((F * (the_arity_of o)) .. f) . e in ( the Sorts of U2 * (the_arity_of o)) . e )
A22: product ( the Sorts of U2 * (the_arity_of o)) <> {} by A2, PRALG_2:3;
assume A23: e in dom ( the Sorts of U2 * (the_arity_of o)) ; ::_thesis: ((F * (the_arity_of o)) .. f) . e in ( the Sorts of U2 * (the_arity_of o)) . e
then A24: e in dom (the_arity_of o) by FUNCT_1:11;
then reconsider g = 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:11, PBOOLE:def_15;
reconsider r = e as Element of NAT by A24;
g = (F * (the_arity_of o)) . e by A20, A23, FUNCT_1:12;
then A25: ((F * (the_arity_of o)) .. f) . e = g . (f . e) by A20, A23, PRALG_1:def_17;
A26: ( the Sorts of U2 * (the_arity_of o)) . e = the Sorts of U2 . ((the_arity_of o) . e) by A24, FUNCT_1:13;
A27: now__::_thesis:_not_the_Sorts_of_U2_._((the_arity_of_o)_._e)_=_{}
assume the Sorts of U2 . ((the_arity_of o) . e) = {} ; ::_thesis: contradiction
then {} in rng ( the Sorts of U2 * (the_arity_of o)) by A23, A26, FUNCT_1:def_3;
hence contradiction by A22, CARD_3:26; ::_thesis: verum
end;
(the_arity_of o) . r in the carrier of S by A24, FINSEQ_2:11;
then (the_arity_of o) . e in dom the Sorts of U1 by PARTFUN1:def_2;
then e in dom ( the Sorts of U1 * (the_arity_of o)) by A24, FUNCT_1:11;
then f . e in (doms (F * (the_arity_of o))) . e by A13, A16;
then f . e in the Sorts of U1 . ((the_arity_of o) . e) by A13, A24, FUNCT_1:13;
then g . (f . e) in the Sorts of U2 . ((the_arity_of o) . e) by A27, FUNCT_2:5;
hence ((F * (the_arity_of o)) .. f) . e in ( the Sorts of U2 * (the_arity_of o)) . e by A23, A25, FUNCT_1:12; ::_thesis: verum
end;
(Frege (F * (the_arity_of o))) . x = (F * (the_arity_of o)) .. f by A14, A13, A15, PRALG_2:def_2;
then (Frege (F * (the_arity_of o))) . x in product ( the Sorts of U2 * (the_arity_of o)) by A17, A20, A21, CARD_3:9;
hence (Frege (F * (the_arity_of o))) . x is Element of Args (o,U2) by PRALG_2:3; ::_thesis: verum
end;
correctness
;
end;
:: deftheorem Def5 defines # MSUALG_3:def_5_:_
for S being non empty non void ManySortedSign
for U1, U2 being MSAlgebra over 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__::_thesis:_for_S_being_non_empty_non_void_ManySortedSign_
for_U1,_U2_being_MSAlgebra_over_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 S be non empty non void ManySortedSign ; ::_thesis: for U1, U2 being MSAlgebra over 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 over S; ::_thesis: 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; ::_thesis: 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; ::_thesis: 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); ::_thesis: 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; ::_thesis: ( 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) ; ::_thesis: ( ( 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_2;
A6: F # x = (Frege (F * (the_arity_of o))) . x by A2, A3, Def5;
A7: dom ( the Sorts of U1 * (the_arity_of o)) = (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o))))
proof
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) c= dom ( the Sorts of U1 * (the_arity_of o))
let e be set ; ::_thesis: ( e in dom ( the Sorts of U1 * (the_arity_of o)) implies e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) )
A8: (F * (the_arity_of o)) . e is Function ;
assume A9: e in dom ( the Sorts of U1 * (the_arity_of o)) ; ::_thesis: e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o))))
then (the_arity_of o) . e in dom the Sorts of U1 by FUNCT_1:11;
then (the_arity_of o) . e in the carrier of S by PARTFUN1:def_2;
then A10: (the_arity_of o) . e in dom F by PARTFUN1:def_2;
e in dom (the_arity_of o) by A9, FUNCT_1:11;
then e in dom (F * (the_arity_of o)) by A10, FUNCT_1:11;
hence e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) by A8, FUNCT_6:19; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) or e in dom ( the Sorts of U1 * (the_arity_of o)) )
assume e in (F * (the_arity_of o)) " (SubFuncs (rng (F * (the_arity_of o)))) ; ::_thesis: e in dom ( the Sorts of U1 * (the_arity_of o))
then e in dom (F * (the_arity_of o)) by FUNCT_6:19;
then A11: e in dom (the_arity_of o) by FUNCT_1:11;
then reconsider f = e as Element of NAT ;
(the_arity_of o) . f in the carrier of S by A11, FINSEQ_2:11;
then (the_arity_of o) . e in dom the Sorts of U1 by PARTFUN1:def_2;
hence e in dom ( the Sorts of U1 * (the_arity_of o)) by A11, FUNCT_1:11; ::_thesis: verum
end;
A12: Args (o,U2) = product ( the Sorts of U2 * (the_arity_of o)) by PRALG_2:3;
then A13: dom u = dom ( the Sorts of U2 * (the_arity_of o)) by A3, CARD_3:9;
A14: Args (o,U1) = product ( the Sorts of U1 * (the_arity_of o)) by PRALG_2:3;
then A15: dom f = dom ( the Sorts of U1 * (the_arity_of o)) by A1, A2, CARD_3:9
.= dom (the_arity_of o) by A5, RELAT_1:27 ;
rng (the_arity_of o) c= dom the Sorts of U2 by A4, PARTFUN1:def_2;
then A16: dom u = dom (the_arity_of o) by A13, RELAT_1:27;
now__::_thesis:_for_e_being_set_st_e_in_(F_*_(the_arity_of_o))_"_(SubFuncs_(rng_(F_*_(the_arity_of_o))))_holds_
(_the_Sorts_of_U1_*_(the_arity_of_o))_._e_=_proj1_((F_*_(the_arity_of_o))_._e)
let e be set ; ::_thesis: ( 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)))) ; ::_thesis: ( 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:19;
then A17: e in dom (the_arity_of o) by FUNCT_1:11;
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:11, PBOOLE:def_15;
( 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_3;
then A18: ( the Sorts of U2 * (the_arity_of o)) . e <> {} by A3, A12, CARD_3:26;
( ( 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:13;
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:13 ;
::_thesis: 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 ::_thesis: ( ( 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 ; ::_thesis: 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, Def5;
let n be Nat; ::_thesis: ( n in dom f implies u . n = (F . ((the_arity_of o) /. n)) . (f . n) )
assume A21: n in dom f ; ::_thesis: 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:11;
then (the_arity_of o) . n in dom F by PARTFUN1:def_2;
then A22: n in dom (F * (the_arity_of o)) by A15, A21, FUNCT_1:11;
then A23: (F * (the_arity_of o)) . n = F . ((the_arity_of o) . n) by FUNCT_1:12
.= F . ((the_arity_of o) /. n) by A15, A21, PARTFUN1:def_6 ;
thus u . n = ((F * (the_arity_of o)) .. f) . n by A1, A2, A14, A19, A20, PRALG_2:def_2
.= (F . ((the_arity_of o) /. n)) . (f . n) by A22, A23, PRALG_1:def_17 ; ::_thesis: verum
end;
F # x is Element of product ( the Sorts of U2 * (the_arity_of o)) by PRALG_2:3;
then reconsider g = F # x as Function ;
A24: rng (the_arity_of o) c= dom F by A4, PARTFUN1:def_2;
assume A25: for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ; ::_thesis: u = F # x
A26: now__::_thesis:_for_e_being_set_st_e_in_dom_f_holds_
u_._e_=_g_._e
let e be set ; ::_thesis: ( e in dom f implies u . e = g . e )
assume A27: e in dom f ; ::_thesis: u . e = g . e
then reconsider n = e as Nat by A15;
(the_arity_of o) . n in the carrier of S by A15, A27, FINSEQ_2:11;
then (the_arity_of o) . n in dom F by PARTFUN1:def_2;
then A28: n in dom (F * (the_arity_of o)) by A15, A27, FUNCT_1:11;
then A29: (F * (the_arity_of o)) . n = F . ((the_arity_of o) . n) by FUNCT_1:12
.= F . ((the_arity_of o) /. n) by A15, A27, PARTFUN1:def_6 ;
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_2 ; ::_thesis: verum
end;
F # x = (F * (the_arity_of o)) .. f by A1, A2, A14, A19, A6, PRALG_2:def_2;
then dom g = dom (F * (the_arity_of o)) by PRALG_1:def_17
.= dom f by A15, A24, RELAT_1:27 ;
hence u = F # x by A15, A16, A26, FUNCT_1:2; ::_thesis: verum
end;
definition
let S be non empty non void ManySortedSign ;
let U1, U2 be non-empty MSAlgebra over S;
let o be OperSymbol of S;
let F be ManySortedFunction of U1,U2;
let x be Element of Args (o,U1);
redefine func F # x means :Def6: :: MSUALG_3:def 6
for n being Nat st n in dom x holds
it . n = (F . ((the_arity_of o) /. n)) . (x . n);
compatibility
for b1 being Element of Args (o,U2) holds
( b1 = F # x iff for n being Nat st n in dom x holds
b1 . n = (F . ((the_arity_of o) /. n)) . (x . n) ) by Lm1;
end;
:: deftheorem Def6 defines # MSUALG_3:def_6_:_
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over 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: :: MSUALG_3:7
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U1 being MSAlgebra over S st Args (o,U1) <> {} holds
for x being Element of Args (o,U1) holds x = (id the Sorts of U1) # x
proof
let S be non empty non void ManySortedSign ; ::_thesis: for o being OperSymbol of S
for U1 being MSAlgebra over S st Args (o,U1) <> {} holds
for x being Element of Args (o,U1) holds x = (id the Sorts of U1) # x
let o be OperSymbol of S; ::_thesis: for U1 being MSAlgebra over S st Args (o,U1) <> {} holds
for x being Element of Args (o,U1) holds x = (id the Sorts of U1) # x
let U1 be MSAlgebra over S; ::_thesis: ( Args (o,U1) <> {} implies for x being Element of Args (o,U1) holds x = (id the Sorts of U1) # x )
set F = id the Sorts of U1;
assume A1: Args (o,U1) <> {} ; ::_thesis: for x being Element of Args (o,U1) holds x = (id the Sorts of U1) # x
then reconsider AA = Args (o,U1) as non empty set ;
let x be Element of Args (o,U1); ::_thesis: x = (id the Sorts of U1) # x
reconsider Fx = (id the Sorts of U1) # x as Element of AA ;
A2: Args (o,U1) = product ( the Sorts of U1 * (the_arity_of o)) by PRALG_2:3;
then consider g being Function such that
A3: Fx = g and
dom g = dom ( the Sorts of U1 * (the_arity_of o)) and
for x being set st x in dom ( the Sorts of U1 * (the_arity_of o)) holds
g . x in ( the Sorts of U1 * (the_arity_of o)) . x by CARD_3:def_5;
consider f being Function such that
A4: x = f and
dom f = dom ( the Sorts of U1 * (the_arity_of o)) and
for x being set st x in dom ( the Sorts of U1 * (the_arity_of o)) holds
f . x in ( the Sorts of U1 * (the_arity_of o)) . x by A1, A2, CARD_3:def_5;
A5: dom f = dom (the_arity_of o) by A4, A3, Th6;
A6: for y being set st y in dom f holds
f . y = g . y
proof
let y be set ; ::_thesis: ( y in dom f implies f . y = g . y )
assume A7: y in dom f ; ::_thesis: f . y = g . y
then reconsider n = y as Nat by A5;
set p = (the_arity_of o) /. n;
dom the Sorts of U1 = the carrier of S by PARTFUN1:def_2;
then rng (the_arity_of o) c= dom the Sorts of U1 by FINSEQ_1:def_4;
then A8: dom ( the Sorts of U1 * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27;
then f . n in ( the Sorts of U1 * (the_arity_of o)) . n by A1, A4, A5, A7, Th6;
then f . n in the Sorts of U1 . ((the_arity_of o) . n) by A5, A7, A8, FUNCT_1:12;
then A9: f . n in the Sorts of U1 . ((the_arity_of o) /. n) by A5, A7, PARTFUN1:def_6;
A10: (id the Sorts of U1) . ((the_arity_of o) /. n) = id ( the Sorts of U1 . ((the_arity_of o) /. n)) by Def1;
g . n = ((id the Sorts of U1) . ((the_arity_of o) /. n)) . (f . n) by A4, A3, A7, Lm1;
hence f . y = g . y by A10, A9, FUNCT_1:18; ::_thesis: verum
end;
dom g = dom (the_arity_of o) by A3, Th6;
hence x = (id the Sorts of U1) # x by A4, A3, A6, Th6, FUNCT_1:2; ::_thesis: verum
end;
theorem Th8: :: MSUALG_3:8
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for U1, U2, U3 being non-empty MSAlgebra over S
for H1 being ManySortedFunction of U1,U2
for H2 being ManySortedFunction of U2,U3
for x being Element of Args (o,U1) holds (H2 ** H1) # x = H2 # (H1 # x)
proof
let S be non empty non void ManySortedSign ; ::_thesis: for o being OperSymbol of S
for U1, U2, U3 being non-empty MSAlgebra over S
for H1 being ManySortedFunction of U1,U2
for H2 being ManySortedFunction of U2,U3
for x being Element of Args (o,U1) holds (H2 ** H1) # x = H2 # (H1 # x)
let o be OperSymbol of S; ::_thesis: for U1, U2, U3 being non-empty MSAlgebra over S
for H1 being ManySortedFunction of U1,U2
for H2 being ManySortedFunction of U2,U3
for x being Element of Args (o,U1) holds (H2 ** H1) # x = H2 # (H1 # x)
let U1, U2, U3 be non-empty MSAlgebra over S; ::_thesis: for H1 being ManySortedFunction of U1,U2
for H2 being ManySortedFunction of U2,U3
for x being Element of Args (o,U1) holds (H2 ** H1) # x = H2 # (H1 # x)
let H1 be ManySortedFunction of U1,U2; ::_thesis: for H2 being ManySortedFunction of U2,U3
for x being Element of Args (o,U1) holds (H2 ** H1) # x = H2 # (H1 # x)
let H2 be ManySortedFunction of U2,U3; ::_thesis: for x being Element of Args (o,U1) holds (H2 ** H1) # x = H2 # (H1 # x)
let x be Element of Args (o,U1); ::_thesis: (H2 ** H1) # x = H2 # (H1 # x)
A1: dom x = dom (the_arity_of o) by Th6;
A2: dom (H1 # x) = dom (the_arity_of o) by Th6;
A3: for y being set st y in dom (the_arity_of o) holds
((H2 ** H1) # x) . y = (H2 # (H1 # x)) . y
proof
rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def_4;
then rng (the_arity_of o) c= dom the Sorts of U1 by PARTFUN1:def_2;
then A4: dom ( the Sorts of U1 * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27;
let y be set ; ::_thesis: ( y in dom (the_arity_of o) implies ((H2 ** H1) # x) . y = (H2 # (H1 # x)) . y )
assume A5: y in dom (the_arity_of o) ; ::_thesis: ((H2 ** H1) # x) . y = (H2 # (H1 # x)) . y
then reconsider n = y as Nat ;
set F = H2 ** H1;
set p = (the_arity_of o) /. n;
A6: ((H2 ** H1) # x) . n = ((H2 ** H1) . ((the_arity_of o) /. n)) . (x . n) by A1, A5, Def6;
(the_arity_of o) /. n = (the_arity_of o) . n by A5, PARTFUN1:def_6;
then A7: ( the Sorts of U1 * (the_arity_of o)) . n = the Sorts of U1 . ((the_arity_of o) /. n) by A5, A4, FUNCT_1:12;
A8: (H2 ** H1) . ((the_arity_of o) /. n) = (H2 . ((the_arity_of o) /. n)) * (H1 . ((the_arity_of o) /. n)) by Th2;
A9: dom (H1 . ((the_arity_of o) /. n)) = the Sorts of U1 . ((the_arity_of o) /. n) by FUNCT_2:def_1;
then dom ((H2 . ((the_arity_of o) /. n)) * (H1 . ((the_arity_of o) /. n))) = dom (H1 . ((the_arity_of o) /. n)) by FUNCT_2:def_1;
hence ((H2 ** H1) # x) . y = (H2 . ((the_arity_of o) /. n)) . ((H1 . ((the_arity_of o) /. n)) . (x . n)) by A5, A6, A4, A9, A7, A8, Th6, FUNCT_1:12
.= (H2 . ((the_arity_of o) /. n)) . ((H1 # x) . n) by A1, A5, Def6
.= (H2 # (H1 # x)) . y by A2, A5, Def6 ;
::_thesis: verum
end;
( dom ((H2 ** H1) # x) = dom (the_arity_of o) & dom (H2 # (H1 # x)) = dom (the_arity_of o) ) by Th6;
hence (H2 ** H1) # x = H2 # (H1 # x) by A3, FUNCT_1:2; ::_thesis: verum
end;
definition
let S be non empty non void ManySortedSign ;
let U1, U2 be MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
predF is_homomorphism U1,U2 means :Def7: :: MSUALG_3:def 7
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);
end;
:: deftheorem Def7 defines is_homomorphism MSUALG_3:def_7_:_
for S being non empty non void ManySortedSign
for U1, U2 being MSAlgebra over 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: :: MSUALG_3:9
for S being non empty non void ManySortedSign
for U1 being MSAlgebra over S holds id the Sorts of U1 is_homomorphism U1,U1
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U1 being MSAlgebra over S holds id the Sorts of U1 is_homomorphism U1,U1
let U1 be MSAlgebra over S; ::_thesis: id the Sorts of U1 is_homomorphism U1,U1
set F = id the Sorts of U1;
let o be OperSymbol of S; :: according to MSUALG_3:def_7 ::_thesis: ( Args (o,U1) <> {} implies for x being Element of Args (o,U1) holds ((id the Sorts of U1) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U1)) . ((id the Sorts of U1) # x) )
assume A1: Args (o,U1) <> {} ; ::_thesis: for x being Element of Args (o,U1) holds ((id the Sorts of U1) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U1)) . ((id the Sorts of U1) # x)
let x be Element of Args (o,U1); ::_thesis: ((id the Sorts of U1) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U1)) . ((id the Sorts of U1) # x)
A2: (id the Sorts of U1) # x = x by A1, Th7;
set r = the_result_sort_of o;
A3: (id the Sorts of U1) . (the_result_sort_of o) = id ( the Sorts of U1 . (the_result_sort_of o)) by Def1;
rng the ResultSort of S c= the carrier of S by RELAT_1:def_19;
then rng the ResultSort of S c= dom the Sorts of U1 by PARTFUN1:def_2;
then A4: ( Result (o,U1) = ( the Sorts of U1 * the ResultSort of S) . o & dom ( the Sorts of U1 * the ResultSort of S) = dom the ResultSort of S ) by MSUALG_1:def_5, RELAT_1:27;
o in the carrier' of S ;
then o in dom the ResultSort of S by FUNCT_2:def_1;
then A5: Result (o,U1) = the Sorts of U1 . ( the ResultSort of S . o) by A4, FUNCT_1:12
.= the Sorts of U1 . (the_result_sort_of o) by MSUALG_1:def_2 ;
percases ( Result (o,U1) <> {} or Result (o,U1) = {} ) ;
suppose Result (o,U1) <> {} ; ::_thesis: ((id the Sorts of U1) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U1)) . ((id the Sorts of U1) # x)
then dom (Den (o,U1)) = Args (o,U1) by FUNCT_2:def_1;
then ( rng (Den (o,U1)) c= Result (o,U1) & (Den (o,U1)) . x in rng (Den (o,U1)) ) by A1, FUNCT_1:def_3, RELAT_1:def_19;
hence ((id the Sorts of U1) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U1)) . ((id the Sorts of U1) # x) by A2, A3, A5, FUNCT_1:18; ::_thesis: verum
end;
supposeA6: Result (o,U1) = {} ; ::_thesis: ((id the Sorts of U1) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U1)) . ((id the Sorts of U1) # x)
then dom (Den (o,U1)) = {} ;
then A7: (Den (o,U1)) . x = {} by FUNCT_1:def_2;
dom ((id the Sorts of U1) . (the_result_sort_of o)) = {} by A5, A6;
then ((id the Sorts of U1) . (the_result_sort_of o)) . {} = {} by FUNCT_1:def_2;
hence ((id the Sorts of U1) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U1)) . ((id the Sorts of U1) # x) by A1, A7, Th7; ::_thesis: verum
end;
end;
end;
theorem Th10: :: MSUALG_3:10
for S being non empty non void ManySortedSign
for U1, U2, U3 being non-empty MSAlgebra over S
for H1 being ManySortedFunction of U1,U2
for H2 being ManySortedFunction of U2,U3 st H1 is_homomorphism U1,U2 & H2 is_homomorphism U2,U3 holds
H2 ** H1 is_homomorphism U1,U3
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2, U3 being non-empty MSAlgebra over S
for H1 being ManySortedFunction of U1,U2
for H2 being ManySortedFunction of U2,U3 st H1 is_homomorphism U1,U2 & H2 is_homomorphism U2,U3 holds
H2 ** H1 is_homomorphism U1,U3
let U1, U2, U3 be non-empty MSAlgebra over S; ::_thesis: for H1 being ManySortedFunction of U1,U2
for H2 being ManySortedFunction of U2,U3 st H1 is_homomorphism U1,U2 & H2 is_homomorphism U2,U3 holds
H2 ** H1 is_homomorphism U1,U3
let H1 be ManySortedFunction of U1,U2; ::_thesis: for H2 being ManySortedFunction of U2,U3 st H1 is_homomorphism U1,U2 & H2 is_homomorphism U2,U3 holds
H2 ** H1 is_homomorphism U1,U3
let H2 be ManySortedFunction of U2,U3; ::_thesis: ( H1 is_homomorphism U1,U2 & H2 is_homomorphism U2,U3 implies H2 ** H1 is_homomorphism U1,U3 )
assume that
A1: H1 is_homomorphism U1,U2 and
A2: H2 is_homomorphism U2,U3 ; ::_thesis: H2 ** H1 is_homomorphism U1,U3
let o be OperSymbol of S; :: according to MSUALG_3:def_7 ::_thesis: ( Args (o,U1) <> {} implies for x being Element of Args (o,U1) holds ((H2 ** H1) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U3)) . ((H2 ** H1) # x) )
assume Args (o,U1) <> {} ; ::_thesis: for x being Element of Args (o,U1) holds ((H2 ** H1) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U3)) . ((H2 ** H1) # x)
let x be Element of Args (o,U1); ::_thesis: ((H2 ** H1) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U3)) . ((H2 ** H1) # x)
set F = H2 ** H1;
set r = the_result_sort_of o;
(H1 . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U2)) . (H1 # x) by A1, Def7;
then A3: (H2 . (the_result_sort_of o)) . ((H1 . (the_result_sort_of o)) . ((Den (o,U1)) . x)) = (Den (o,U3)) . (H2 # (H1 # x)) by A2, Def7;
A4: ( (H2 ** H1) . (the_result_sort_of o) = (H2 . (the_result_sort_of o)) * (H1 . (the_result_sort_of o)) & dom ((H2 ** H1) . (the_result_sort_of o)) = the Sorts of U1 . (the_result_sort_of o) ) by Th2, FUNCT_2:def_1;
rng the ResultSort of S c= the carrier of S by RELAT_1:def_19;
then rng the ResultSort of S c= dom the Sorts of U1 by PARTFUN1:def_2;
then A5: ( Result (o,U1) = ( the Sorts of U1 * the ResultSort of S) . o & dom ( the Sorts of U1 * the ResultSort of S) = dom the ResultSort of S ) by MSUALG_1:def_5, RELAT_1:27;
o in the carrier' of S ;
then o in dom the ResultSort of S by FUNCT_2:def_1;
then Result (o,U1) = the Sorts of U1 . ( the ResultSort of S . o) by A5, FUNCT_1:12
.= the Sorts of U1 . (the_result_sort_of o) by MSUALG_1:def_2 ;
then ((H2 ** H1) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U3)) . (H2 # (H1 # x)) by A3, A4, FUNCT_1:12;
hence ((H2 ** H1) . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U3)) . ((H2 ** H1) # x) by Th8; ::_thesis: verum
end;
definition
let S be non empty non void ManySortedSign ;
let U1, U2 be MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
predF is_epimorphism U1,U2 means :Def8: :: MSUALG_3:def 8
( F is_homomorphism U1,U2 & F is "onto" );
end;
:: deftheorem Def8 defines is_epimorphism MSUALG_3:def_8_:_
for S being non empty non void ManySortedSign
for U1, U2 being MSAlgebra over 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: :: MSUALG_3:11
for S being non empty non void ManySortedSign
for U1, U2, U3 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U2,U3 st F is_epimorphism U1,U2 & G is_epimorphism U2,U3 holds
G ** F is_epimorphism U1,U3
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2, U3 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U2,U3 st F is_epimorphism U1,U2 & G is_epimorphism U2,U3 holds
G ** F is_epimorphism U1,U3
let U1, U2, U3 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U2,U3 st F is_epimorphism U1,U2 & G is_epimorphism U2,U3 holds
G ** F is_epimorphism U1,U3
let F be ManySortedFunction of U1,U2; ::_thesis: for G being ManySortedFunction of U2,U3 st F is_epimorphism U1,U2 & G is_epimorphism U2,U3 holds
G ** F is_epimorphism U1,U3
let G be ManySortedFunction of U2,U3; ::_thesis: ( F is_epimorphism U1,U2 & G is_epimorphism U2,U3 implies G ** F is_epimorphism U1,U3 )
assume that
A1: F is_epimorphism U1,U2 and
A2: G is_epimorphism U2,U3 ; ::_thesis: G ** F is_epimorphism U1,U3
A3: G is "onto" by A2, Def8;
A4: F is "onto" by A1, Def8;
for i being set st i in the carrier of S holds
rng ((G ** F) . i) = the Sorts of U3 . i
proof
let i be set ; ::_thesis: ( i in the carrier of S implies rng ((G ** F) . i) = the Sorts of U3 . i )
assume A5: i in the carrier of S ; ::_thesis: rng ((G ** F) . i) = the Sorts of U3 . i
then reconsider f = F . i as Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) by PBOOLE:def_15;
reconsider g = G . i as Function of ( the Sorts of U2 . i),( the Sorts of U3 . i) by A5, PBOOLE:def_15;
rng f = the Sorts of U2 . i by A4, A5, Def3;
then A6: dom g = rng f by A5, FUNCT_2:def_1;
rng g = the Sorts of U3 . i by A3, A5, Def3;
then rng (g * f) = the Sorts of U3 . i by A6, RELAT_1:28;
hence rng ((G ** F) . i) = the Sorts of U3 . i by A5, Th2; ::_thesis: verum
end;
then A7: G ** F is "onto" by Def3;
( F is_homomorphism U1,U2 & G is_homomorphism U2,U3 ) by A1, A2, Def8;
then G ** F is_homomorphism U1,U3 by Th10;
hence G ** F is_epimorphism U1,U3 by A7, Def8; ::_thesis: verum
end;
definition
let S be non empty non void ManySortedSign ;
let U1, U2 be MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
predF is_monomorphism U1,U2 means :Def9: :: MSUALG_3:def 9
( F is_homomorphism U1,U2 & F is "1-1" );
end;
:: deftheorem Def9 defines is_monomorphism MSUALG_3:def_9_:_
for S being non empty non void ManySortedSign
for U1, U2 being MSAlgebra over 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: :: MSUALG_3:12
for S being non empty non void ManySortedSign
for U1, U2, U3 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U2,U3 st F is_monomorphism U1,U2 & G is_monomorphism U2,U3 holds
G ** F is_monomorphism U1,U3
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2, U3 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U2,U3 st F is_monomorphism U1,U2 & G is_monomorphism U2,U3 holds
G ** F is_monomorphism U1,U3
let U1, U2, U3 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U2,U3 st F is_monomorphism U1,U2 & G is_monomorphism U2,U3 holds
G ** F is_monomorphism U1,U3
let F be ManySortedFunction of U1,U2; ::_thesis: for G being ManySortedFunction of U2,U3 st F is_monomorphism U1,U2 & G is_monomorphism U2,U3 holds
G ** F is_monomorphism U1,U3
let G be ManySortedFunction of U2,U3; ::_thesis: ( F is_monomorphism U1,U2 & G is_monomorphism U2,U3 implies G ** F is_monomorphism U1,U3 )
assume that
A1: F is_monomorphism U1,U2 and
A2: G is_monomorphism U2,U3 ; ::_thesis: G ** F is_monomorphism U1,U3
A3: G is "1-1" by A2, Def9;
A4: F is "1-1" by A1, Def9;
for i being set
for h being Function st i in dom (G ** F) & (G ** F) . i = h holds
h is one-to-one
proof
let i be set ; ::_thesis: for h being Function st i in dom (G ** F) & (G ** F) . i = h holds
h is one-to-one
let h be Function; ::_thesis: ( i in dom (G ** F) & (G ** F) . i = h implies h is one-to-one )
assume that
A5: i in dom (G ** F) and
A6: (G ** F) . i = h ; ::_thesis: h is one-to-one
A7: i in the carrier of S by A5, PARTFUN1:def_2;
then reconsider g = G . i as Function of ( the Sorts of U2 . i),( the Sorts of U3 . i) by PBOOLE:def_15;
reconsider f = F . i as Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) by A7, PBOOLE:def_15;
i in dom G by A7, PARTFUN1:def_2;
then A8: g is one-to-one by A3, Def2;
i in dom F by A7, PARTFUN1:def_2;
then f is one-to-one by A4, Def2;
then g * f is one-to-one by A8;
hence h is one-to-one by A6, A7, Th2; ::_thesis: verum
end;
then A9: G ** F is "1-1" by Def2;
( F is_homomorphism U1,U2 & G is_homomorphism U2,U3 ) by A1, A2, Def9;
then G ** F is_homomorphism U1,U3 by Th10;
hence G ** F is_monomorphism U1,U3 by A9, Def9; ::_thesis: verum
end;
definition
let S be non empty non void ManySortedSign ;
let U1, U2 be MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
predF is_isomorphism U1,U2 means :Def10: :: MSUALG_3:def 10
( F is_epimorphism U1,U2 & F is_monomorphism U1,U2 );
end;
:: deftheorem Def10 defines is_isomorphism MSUALG_3:def_10_:_
for S being non empty non void ManySortedSign
for U1, U2 being MSAlgebra over 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: :: MSUALG_3:13
for S being non empty non void ManySortedSign
for U1, U2 being MSAlgebra over S
for F being ManySortedFunction of U1,U2 holds
( F is_isomorphism U1,U2 iff ( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" ) )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2 being MSAlgebra over S
for F being ManySortedFunction of U1,U2 holds
( F is_isomorphism U1,U2 iff ( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" ) )
let U1, U2 be MSAlgebra over S; ::_thesis: for F being ManySortedFunction of U1,U2 holds
( F is_isomorphism U1,U2 iff ( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" ) )
let F be ManySortedFunction of U1,U2; ::_thesis: ( F is_isomorphism U1,U2 iff ( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" ) )
thus ( F is_isomorphism U1,U2 implies ( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" ) ) ::_thesis: ( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" implies F is_isomorphism U1,U2 )
proof
assume F is_isomorphism U1,U2 ; ::_thesis: ( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" )
then ( F is_epimorphism U1,U2 & F is_monomorphism U1,U2 ) by Def10;
hence ( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" ) by Def8, Def9; ::_thesis: verum
end;
assume ( F is_homomorphism U1,U2 & F is "onto" & F is "1-1" ) ; ::_thesis: F is_isomorphism U1,U2
then ( F is_epimorphism U1,U2 & F is_monomorphism U1,U2 ) by Def8, Def9;
hence F is_isomorphism U1,U2 by Def10; ::_thesis: verum
end;
Lm2: for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for H being ManySortedFunction of U1,U2 st H is_isomorphism U1,U2 holds
H "" is_homomorphism U2,U1
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2 being non-empty MSAlgebra over S
for H being ManySortedFunction of U1,U2 st H is_isomorphism U1,U2 holds
H "" is_homomorphism U2,U1
let U1, U2 be non-empty MSAlgebra over S; ::_thesis: for H being ManySortedFunction of U1,U2 st H is_isomorphism U1,U2 holds
H "" is_homomorphism U2,U1
let H be ManySortedFunction of U1,U2; ::_thesis: ( H is_isomorphism U1,U2 implies H "" is_homomorphism U2,U1 )
set F = H "" ;
assume A1: H is_isomorphism U1,U2 ; ::_thesis: H "" is_homomorphism U2,U1
then A2: H is "onto" by Th13;
A3: H is "1-1" by A1, Th13;
A4: H is_homomorphism U1,U2 by A1, Th13;
for o being OperSymbol of S st Args (o,U2) <> {} holds
for x being Element of Args (o,U2) holds ((H "") . (the_result_sort_of o)) . ((Den (o,U2)) . x) = (Den (o,U1)) . ((H "") # x)
proof
let o be OperSymbol of S; ::_thesis: ( Args (o,U2) <> {} implies for x being Element of Args (o,U2) holds ((H "") . (the_result_sort_of o)) . ((Den (o,U2)) . x) = (Den (o,U1)) . ((H "") # x) )
assume Args (o,U2) <> {} ; ::_thesis: for x being Element of Args (o,U2) holds ((H "") . (the_result_sort_of o)) . ((Den (o,U2)) . x) = (Den (o,U1)) . ((H "") # x)
let x be Element of Args (o,U2); ::_thesis: ((H "") . (the_result_sort_of o)) . ((Den (o,U2)) . x) = (Den (o,U1)) . ((H "") # x)
set r = the_result_sort_of o;
deffunc H1( set ) -> set = ((H "") # x) . $1;
consider f being Function such that
A5: ( dom f = dom (the_arity_of o) & ( for n being set st n in dom (the_arity_of o) holds
f . n = H1(n) ) ) from FUNCT_1:sch_3();
A6: dom ((H "") # x) = dom (the_arity_of o) by Th6;
then A7: f = (H "") # x by A5, FUNCT_1:2;
the_result_sort_of o in the carrier of S ;
then the_result_sort_of o in dom H by PARTFUN1:def_2;
then A8: H . (the_result_sort_of o) is one-to-one by A3, Def2;
( dom (H . (the_result_sort_of o)) = the Sorts of U1 . (the_result_sort_of o) & (H "") . (the_result_sort_of o) = (H . (the_result_sort_of o)) " ) by A2, A3, Def4, FUNCT_2:def_1;
then A9: ((H "") . (the_result_sort_of o)) * (H . (the_result_sort_of o)) = id ( the Sorts of U1 . (the_result_sort_of o)) by A8, FUNCT_1:39;
A10: dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1;
then A11: dom ( the Sorts of U1 * the ResultSort of S) = dom the ResultSort of S by PARTFUN1:def_2;
A12: Result (o,U1) = ( the Sorts of U1 * the ResultSort of S) . o by MSUALG_1:def_5
.= the Sorts of U1 . ( the ResultSort of S . o) by A10, A11, FUNCT_1:12
.= the Sorts of U1 . (the_result_sort_of o) by MSUALG_1:def_2 ;
reconsider f = f as Element of Args (o,U1) by A5, A6, FUNCT_1:2;
A13: dom (((H "") . (the_result_sort_of o)) * (H . (the_result_sort_of o))) = the Sorts of U1 . (the_result_sort_of o) by FUNCT_2:def_1;
(H . (the_result_sort_of o)) . ((Den (o,U1)) . f) = (Den (o,U2)) . (H # ((H "") # x)) by A4, A7, Def7
.= (Den (o,U2)) . ((H ** (H "")) # x) by Th8
.= (Den (o,U2)) . ((id the Sorts of U2) # x) by A2, A3, Th5
.= (Den (o,U2)) . x by Th7 ;
then ((H "") . (the_result_sort_of o)) . ((Den (o,U2)) . x) = (((H "") . (the_result_sort_of o)) * (H . (the_result_sort_of o))) . ((Den (o,U1)) . ((H "") # x)) by A7, A13, A12, FUNCT_1:12
.= (Den (o,U1)) . ((H "") # x) by A12, A9, FUNCT_1:18 ;
hence ((H "") . (the_result_sort_of o)) . ((Den (o,U2)) . x) = (Den (o,U1)) . ((H "") # x) ; ::_thesis: verum
end;
hence H "" is_homomorphism U2,U1 by Def7; ::_thesis: verum
end;
theorem Th14: :: MSUALG_3:14
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for H being ManySortedFunction of U1,U2
for H1 being ManySortedFunction of U2,U1 st H is_isomorphism U1,U2 & H1 = H "" holds
H1 is_isomorphism U2,U1
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2 being non-empty MSAlgebra over S
for H being ManySortedFunction of U1,U2
for H1 being ManySortedFunction of U2,U1 st H is_isomorphism U1,U2 & H1 = H "" holds
H1 is_isomorphism U2,U1
let U1, U2 be non-empty MSAlgebra over S; ::_thesis: for H being ManySortedFunction of U1,U2
for H1 being ManySortedFunction of U2,U1 st H is_isomorphism U1,U2 & H1 = H "" holds
H1 is_isomorphism U2,U1
let H be ManySortedFunction of U1,U2; ::_thesis: for H1 being ManySortedFunction of U2,U1 st H is_isomorphism U1,U2 & H1 = H "" holds
H1 is_isomorphism U2,U1
let H1 be ManySortedFunction of U2,U1; ::_thesis: ( H is_isomorphism U1,U2 & H1 = H "" implies H1 is_isomorphism U2,U1 )
assume that
A1: H is_isomorphism U1,U2 and
A2: H1 = H "" ; ::_thesis: H1 is_isomorphism U2,U1
A3: H1 is_homomorphism U2,U1 by A1, A2, Lm2;
H is_monomorphism U1,U2 by A1, Def10;
then A4: H is "1-1" by Def9;
H is_epimorphism U1,U2 by A1, Def10;
then A5: H is "onto" by Def8;
for i being set
for g being Function st i in dom H1 & g = H1 . i holds
g is one-to-one
proof
let i be set ; ::_thesis: for g being Function st i in dom H1 & g = H1 . i holds
g is one-to-one
let g be Function; ::_thesis: ( i in dom H1 & g = H1 . i implies g is one-to-one )
assume that
A6: i in dom H1 and
A7: g = H1 . i ; ::_thesis: g is one-to-one
A8: i in the carrier of S by A6, PARTFUN1:def_2;
then reconsider f = H . i as Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) by PBOOLE:def_15;
i in dom H by A8, PARTFUN1:def_2;
then f is one-to-one by A4, Def2;
then f " is one-to-one ;
hence g is one-to-one by A2, A4, A5, A7, A8, Def4; ::_thesis: verum
end;
then H1 is "1-1" by Def2;
then A9: H1 is_monomorphism U2,U1 by A3, Def9;
for i being set st i in the carrier of S holds
rng (H1 . i) = the Sorts of U1 . i
proof
let i be set ; ::_thesis: ( i in the carrier of S implies rng (H1 . i) = the Sorts of U1 . i )
assume A10: i in the carrier of S ; ::_thesis: rng (H1 . i) = the Sorts of U1 . i
then reconsider f = H . i as Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) by PBOOLE:def_15;
i in dom H by A10, PARTFUN1:def_2;
then f is one-to-one by A4, Def2;
then rng (f ") = dom f by FUNCT_1:33;
then rng (f ") = the Sorts of U1 . i by A10, FUNCT_2:def_1;
hence rng (H1 . i) = the Sorts of U1 . i by A2, A4, A5, A10, Def4; ::_thesis: verum
end;
then H1 is "onto" by Def3;
then H1 is_epimorphism U2,U1 by A3, Def8;
hence H1 is_isomorphism U2,U1 by A9, Def10; ::_thesis: verum
end;
theorem Th15: :: MSUALG_3:15
for S being non empty non void ManySortedSign
for U1, U2, U3 being non-empty MSAlgebra over S
for H being ManySortedFunction of U1,U2
for H1 being ManySortedFunction of U2,U3 st H is_isomorphism U1,U2 & H1 is_isomorphism U2,U3 holds
H1 ** H is_isomorphism U1,U3
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2, U3 being non-empty MSAlgebra over S
for H being ManySortedFunction of U1,U2
for H1 being ManySortedFunction of U2,U3 st H is_isomorphism U1,U2 & H1 is_isomorphism U2,U3 holds
H1 ** H is_isomorphism U1,U3
let U1, U2, U3 be non-empty MSAlgebra over S; ::_thesis: for H being ManySortedFunction of U1,U2
for H1 being ManySortedFunction of U2,U3 st H is_isomorphism U1,U2 & H1 is_isomorphism U2,U3 holds
H1 ** H is_isomorphism U1,U3
let H be ManySortedFunction of U1,U2; ::_thesis: for H1 being ManySortedFunction of U2,U3 st H is_isomorphism U1,U2 & H1 is_isomorphism U2,U3 holds
H1 ** H is_isomorphism U1,U3
let H1 be ManySortedFunction of U2,U3; ::_thesis: ( H is_isomorphism U1,U2 & H1 is_isomorphism U2,U3 implies H1 ** H is_isomorphism U1,U3 )
assume A1: ( H is_isomorphism U1,U2 & H1 is_isomorphism U2,U3 ) ; ::_thesis: H1 ** H is_isomorphism U1,U3
then ( H is_epimorphism U1,U2 & H1 is_epimorphism U2,U3 ) by Def10;
then A2: H1 ** H is_epimorphism U1,U3 by Th11;
( H is_monomorphism U1,U2 & H1 is_monomorphism U2,U3 ) by A1, Def10;
then H1 ** H is_monomorphism U1,U3 by Th12;
hence H1 ** H is_isomorphism U1,U3 by A2, Def10; ::_thesis: verum
end;
definition
let S be non empty non void ManySortedSign ;
let U1, U2 be MSAlgebra over S;
predU1,U2 are_isomorphic means :Def11: :: MSUALG_3:def 11
ex F being ManySortedFunction of U1,U2 st F is_isomorphism U1,U2;
end;
:: deftheorem Def11 defines are_isomorphic MSUALG_3:def_11_:_
for S being non empty non void ManySortedSign
for U1, U2 being MSAlgebra over S holds
( U1,U2 are_isomorphic iff ex F being ManySortedFunction of U1,U2 st F is_isomorphism U1,U2 );
theorem Th16: :: MSUALG_3:16
for S being non empty non void ManySortedSign
for U1 being MSAlgebra over S holds
( id the Sorts of U1 is_isomorphism U1,U1 & U1,U1 are_isomorphic )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U1 being MSAlgebra over S holds
( id the Sorts of U1 is_isomorphism U1,U1 & U1,U1 are_isomorphic )
let U1 be MSAlgebra over S; ::_thesis: ( id the Sorts of U1 is_isomorphism U1,U1 & U1,U1 are_isomorphic )
A1: id the Sorts of U1 is_homomorphism U1,U1 by Th9;
for i being set
for f being Function st i in dom (id the Sorts of U1) & (id the Sorts of U1) . i = f holds
f is one-to-one
proof
let i be set ; ::_thesis: for f being Function st i in dom (id the Sorts of U1) & (id the Sorts of U1) . i = f holds
f is one-to-one
let f be Function; ::_thesis: ( i in dom (id the Sorts of U1) & (id the Sorts of U1) . i = f implies f is one-to-one )
assume that
A2: i in dom (id the Sorts of U1) and
A3: (id the Sorts of U1) . i = f ; ::_thesis: f is one-to-one
i in the carrier of S by A2, PARTFUN1:def_2;
then f = id ( the Sorts of U1 . i) by A3, Def1;
hence f is one-to-one ; ::_thesis: verum
end;
then id the Sorts of U1 is "1-1" by Def2;
then A4: id the Sorts of U1 is_monomorphism U1,U1 by A1, Def9;
for i being set st i in the carrier of S holds
rng ((id the Sorts of U1) . i) = the Sorts of U1 . i
proof
let i be set ; ::_thesis: ( i in the carrier of S implies rng ((id the Sorts of U1) . i) = the Sorts of U1 . i )
assume i in the carrier of S ; ::_thesis: rng ((id the Sorts of U1) . i) = the Sorts of U1 . i
then (id the Sorts of U1) . i = id ( the Sorts of U1 . i) by Def1;
hence rng ((id the Sorts of U1) . i) = the Sorts of U1 . i by RELAT_1:45; ::_thesis: verum
end;
then id the Sorts of U1 is "onto" by Def3;
then A5: id the Sorts of U1 is_epimorphism U1,U1 by A1, Def8;
hence id the Sorts of U1 is_isomorphism U1,U1 by A4, Def10; ::_thesis: U1,U1 are_isomorphic
take id the Sorts of U1 ; :: according to MSUALG_3:def_11 ::_thesis: id the Sorts of U1 is_isomorphism U1,U1
thus id the Sorts of U1 is_isomorphism U1,U1 by A4, A5, Def10; ::_thesis: verum
end;
definition
let S be non empty non void ManySortedSign ;
let U1, U2 be MSAlgebra over S;
:: original: are_isomorphic
redefine predU1,U2 are_isomorphic ;
reflexivity
for U1 being MSAlgebra over S holds (S,b1,b1) by Th16;
end;
theorem :: MSUALG_3:17
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S st U1,U2 are_isomorphic holds
U2,U1 are_isomorphic
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2 being non-empty MSAlgebra over S st U1,U2 are_isomorphic holds
U2,U1 are_isomorphic
let U1, U2 be non-empty MSAlgebra over S; ::_thesis: ( U1,U2 are_isomorphic implies U2,U1 are_isomorphic )
assume U1,U2 are_isomorphic ; ::_thesis: U2,U1 are_isomorphic
then consider F being ManySortedFunction of U1,U2 such that
A1: F is_isomorphism U1,U2 by Def11;
reconsider G = F "" as ManySortedFunction of U2,U1 ;
G is_isomorphism U2,U1 by A1, Th14;
hence U2,U1 are_isomorphic by Def11; ::_thesis: verum
end;
theorem :: MSUALG_3:18
for S being non empty non void ManySortedSign
for U1, U2, U3 being non-empty MSAlgebra over S st U1,U2 are_isomorphic & U2,U3 are_isomorphic holds
U1,U3 are_isomorphic
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2, U3 being non-empty MSAlgebra over S st U1,U2 are_isomorphic & U2,U3 are_isomorphic holds
U1,U3 are_isomorphic
let U1, U2, U3 be non-empty MSAlgebra over S; ::_thesis: ( U1,U2 are_isomorphic & U2,U3 are_isomorphic implies U1,U3 are_isomorphic )
assume that
A1: U1,U2 are_isomorphic and
A2: U2,U3 are_isomorphic ; ::_thesis: U1,U3 are_isomorphic
consider F being ManySortedFunction of U1,U2 such that
A3: F is_isomorphism U1,U2 by A1, Def11;
consider G being ManySortedFunction of U2,U3 such that
A4: G is_isomorphism U2,U3 by A2, Def11;
reconsider H = G ** F as ManySortedFunction of U1,U3 ;
H is_isomorphism U1,U3 by A3, A4, Th15;
hence U1,U3 are_isomorphic by Def11; ::_thesis: verum
end;
definition
let S be non empty non void ManySortedSign ;
let U1, U2 be non-empty MSAlgebra over S;
let F be ManySortedFunction of U1,U2;
assume A1: F is_homomorphism U1,U2 ;
func Image F -> strict non-empty MSSubAlgebra of U2 means :Def12: :: MSUALG_3:def 12
the Sorts of it = F .:.: the Sorts of U1;
existence
ex b1 being strict non-empty MSSubAlgebra of U2 st the Sorts of b1 = F .:.: the Sorts of U1
proof
set u2 = F .:.: the Sorts of U1;
A2: now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_
not_(F_.:.:_the_Sorts_of_U1)_._i_is_empty
let i be set ; ::_thesis: ( i in the carrier of S implies not (F .:.: the Sorts of U1) . i is empty )
reconsider f = F . i as Function ;
assume A3: i in the carrier of S ; ::_thesis: not (F .:.: the Sorts of U1) . i is empty
then A4: (F .:.: the Sorts of U1) . i = f .: ( the Sorts of U1 . i) by PBOOLE:def_20;
reconsider f = f as Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) by A3, PBOOLE:def_15;
dom f = the Sorts of U1 . i by A3, FUNCT_2:def_1;
hence not (F .:.: the Sorts of U1) . i is empty by A3, A4, RELAT_1:119; ::_thesis: verum
end;
now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_
(F_.:.:_the_Sorts_of_U1)_._i_c=_the_Sorts_of_U2_._i
let i be set ; ::_thesis: ( i in the carrier of S implies (F .:.: the Sorts of U1) . i c= the Sorts of U2 . i )
reconsider f = F . i as Function ;
assume A5: i in the carrier of S ; ::_thesis: (F .:.: the Sorts of U1) . i c= the Sorts of U2 . i
then A6: (F .:.: the Sorts of U1) . i = f .: ( the Sorts of U1 . i) by PBOOLE:def_20;
reconsider f = f as Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) by A5, PBOOLE:def_15;
A7: rng f c= the Sorts of U2 . i by RELAT_1:def_19;
dom f = the Sorts of U1 . i by A5, FUNCT_2:def_1;
hence (F .:.: the Sorts of U1) . i c= the Sorts of U2 . i by A6, A7, RELAT_1:113; ::_thesis: verum
end;
then F .:.: the Sorts of U1 c= the Sorts of U2 by PBOOLE:def_2;
then reconsider u2 = F .:.: the Sorts of U1 as V2() MSSubset of U2 by A2, PBOOLE:def_13, PBOOLE:def_18;
set M = GenMSAlg u2;
reconsider M9 = MSAlgebra(# u2,(Opers (U2,u2)) #) as non-empty MSAlgebra over S by MSUALG_1:def_3;
take GenMSAlg u2 ; ::_thesis: the Sorts of (GenMSAlg u2) = F .:.: the Sorts of U1
u2 is opers_closed
proof
let o be OperSymbol of S; :: according to MSUALG_2:def_6 ::_thesis: u2 is_closed_on o
thus rng ((Den (o,U2)) | (((u2 #) * the Arity of S) . o)) c= (u2 * the ResultSort of S) . o :: according to MSUALG_2:def_5 ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng ((Den (o,U2)) | (((u2 #) * the Arity of S) . o)) or x in (u2 * the ResultSort of S) . o )
set D = Den (o,U2);
set X = ((u2 #) * the Arity of S) . o;
set ao = the_arity_of o;
set ro = the_result_sort_of o;
set ut = u2 * (the_arity_of o);
set S1 = the Sorts of U1;
A8: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def_4;
A9: dom the Arity of S = the carrier' of S by FUNCT_2:def_1;
then dom ((u2 #) * the Arity of S) = dom the Arity of S by PARTFUN1:def_2;
then A10: ((u2 #) * the Arity of S) . o = (u2 #) . ( the Arity of S . o) by A9, FUNCT_1:12
.= (u2 #) . (the_arity_of o) by MSUALG_1:def_1
.= product (u2 * (the_arity_of o)) by FINSEQ_2:def_5 ;
assume x in rng ((Den (o,U2)) | (((u2 #) * the Arity of S) . o)) ; ::_thesis: x in (u2 * the ResultSort of S) . o
then consider a being set such that
A11: a in dom ((Den (o,U2)) | (((u2 #) * the Arity of S) . o)) and
A12: x = ((Den (o,U2)) | (((u2 #) * the Arity of S) . o)) . a by FUNCT_1:def_3;
A13: x = (Den (o,U2)) . a by A11, A12, FUNCT_1:47;
dom ((Den (o,U2)) | (((u2 #) * the Arity of S) . o)) c= dom (Den (o,U2)) by RELAT_1:60;
then reconsider a = a as Element of Args (o,U2) by A11, FUNCT_2:def_1;
defpred S1[ set , set ] means for s being SortSymbol of S st s = (the_arity_of o) . $1 holds
( $2 in the Sorts of U1 . s & a . $1 = (F . s) . $2 );
A14: dom ((Den (o,U2)) | (((u2 #) * the Arity of S) . o)) c= ((u2 #) * the Arity of S) . o by RELAT_1:58;
then A15: dom a = dom (u2 * (the_arity_of o)) by A11, A10, CARD_3:9;
A16: dom u2 = the carrier of S by PARTFUN1:def_2;
A17: for y being set st y in dom a holds
ex i being set st S1[y,i]
proof
let y be set ; ::_thesis: ( y in dom a implies ex i being set st S1[y,i] )
assume A18: y in dom a ; ::_thesis: ex i being set st S1[y,i]
then A19: a . y in (u2 * (the_arity_of o)) . y by A11, A14, A10, A15, CARD_3:9;
dom (u2 * (the_arity_of o)) = dom (the_arity_of o) by A16, A8, RELAT_1:27;
then (the_arity_of o) . y in rng (the_arity_of o) by A15, A18, FUNCT_1:def_3;
then reconsider s = (the_arity_of o) . y as SortSymbol of S by A8;
A20: dom (F . s) = the Sorts of U1 . s by FUNCT_2:def_1;
(u2 * (the_arity_of o)) . y = u2 . ((the_arity_of o) . y) by A15, A18, FUNCT_1:12
.= (F . s) .: ( the Sorts of U1 . s) by PBOOLE:def_20
.= rng (F . s) by A20, RELAT_1:113 ;
then consider i being set such that
A21: ( i in the Sorts of U1 . s & a . y = (F . s) . i ) by A20, A19, FUNCT_1:def_3;
take i ; ::_thesis: S1[y,i]
thus S1[y,i] by A21; ::_thesis: verum
end;
consider f being Function such that
A22: ( dom f = dom a & ( for y being set st y in dom a holds
S1[y,f . y] ) ) from CLASSES1:sch_1(A17);
dom the Sorts of U1 = the carrier of S by PARTFUN1:def_2;
then A23: dom ( the Sorts of U1 * (the_arity_of o)) = dom (the_arity_of o) by A8, RELAT_1:27;
A24: dom f = dom (the_arity_of o) by A15, A16, A8, A22, RELAT_1:27;
A25: for y being set st y in dom ( the Sorts of U1 * (the_arity_of o)) holds
f . y in ( the Sorts of U1 * (the_arity_of o)) . y
proof
let y be set ; ::_thesis: ( y in dom ( the Sorts of U1 * (the_arity_of o)) implies f . y in ( the Sorts of U1 * (the_arity_of o)) . y )
assume A26: y in dom ( the Sorts of U1 * (the_arity_of o)) ; ::_thesis: f . y in ( the Sorts of U1 * (the_arity_of o)) . y
then (the_arity_of o) . y in rng (the_arity_of o) by A23, FUNCT_1:def_3;
then reconsider s = (the_arity_of o) . y as SortSymbol of S by A8;
f . y in the Sorts of U1 . s by A22, A24, A23, A26;
hence f . y in ( the Sorts of U1 * (the_arity_of o)) . y by A26, FUNCT_1:12; ::_thesis: verum
end;
Args (o,U1) = product ( the Sorts of U1 * (the_arity_of o)) by PRALG_2:3;
then reconsider a1 = f as Element of Args (o,U1) by A24, A23, A25, CARD_3:9;
A27: dom a1 = dom (the_arity_of o) by Th6;
A28: now__::_thesis:_for_y_being_set_st_y_in_dom_(the_arity_of_o)_holds_
(F_#_a1)_._y_=_a_._y
let y be set ; ::_thesis: ( y in dom (the_arity_of o) implies (F # a1) . y = a . y )
assume A29: y in dom (the_arity_of o) ; ::_thesis: (F # a1) . y = a . y
then reconsider n = y as Nat ;
(the_arity_of o) . y in rng (the_arity_of o) by A29, FUNCT_1:def_3;
then reconsider s = (the_arity_of o) . y as SortSymbol of S by A8;
(F # a1) . n = (F . ((the_arity_of o) /. n)) . (a1 . n) by A27, A29, Def6
.= (F . s) . (a1 . n) by A29, PARTFUN1:def_6 ;
hence (F # a1) . y = a . y by A22, A27, A29; ::_thesis: verum
end;
( dom (F # a1) = dom (the_arity_of o) & dom a = dom (the_arity_of o) ) by Th6;
then F # a1 = a by A28, FUNCT_1:2;
then A30: (F . (the_result_sort_of o)) . ((Den (o,U1)) . a1) = x by A1, A13, Def7;
reconsider g = F . (the_result_sort_of o) as Function ;
A31: dom (F . (the_result_sort_of o)) = the Sorts of U1 . (the_result_sort_of o) by FUNCT_2:def_1;
A32: dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1;
then A33: dom ( the Sorts of U1 * the ResultSort of S) = dom the ResultSort of S by PARTFUN1:def_2;
Result (o,U1) = ( the Sorts of U1 * the ResultSort of S) . o by MSUALG_1:def_5
.= the Sorts of U1 . ( the ResultSort of S . o) by A32, A33, FUNCT_1:12
.= the Sorts of U1 . (the_result_sort_of o) by MSUALG_1:def_2 ;
then (Den (o,U1)) . a1 in the Sorts of U1 . (the_result_sort_of o) ;
then A34: (Den (o,U1)) . a1 in dom (F . (the_result_sort_of o)) by FUNCT_2:def_1;
dom (u2 * the ResultSort of S) = dom the ResultSort of S by A32, PARTFUN1:def_2;
then (u2 * the ResultSort of S) . o = u2 . ( the ResultSort of S . o) by A32, FUNCT_1:12
.= u2 . (the_result_sort_of o) by MSUALG_1:def_2
.= g .: ( the Sorts of U1 . (the_result_sort_of o)) by PBOOLE:def_20
.= rng g by A31, RELAT_1:113 ;
hence x in (u2 * the ResultSort of S) . o by A30, A34, FUNCT_1:def_3; ::_thesis: verum
end;
end;
then for B being MSSubset of U2 st B = the Sorts of M9 holds
( B is opers_closed & the Charact of M9 = Opers (U2,B) ) ;
then A35: M9 is MSSubAlgebra of U2 by MSUALG_2:def_9;
u2 is MSSubset of M9 by PBOOLE:def_18;
then GenMSAlg u2 is MSSubAlgebra of M9 by A35, MSUALG_2:def_17;
then the Sorts of (GenMSAlg u2) is MSSubset of M9 by MSUALG_2:def_9;
then A36: the Sorts of (GenMSAlg u2) c= u2 by PBOOLE:def_18;
u2 is MSSubset of (GenMSAlg u2) by MSUALG_2:def_17;
then u2 c= the Sorts of (GenMSAlg u2) by PBOOLE:def_18;
hence the Sorts of (GenMSAlg u2) = F .:.: the Sorts of U1 by A36, PBOOLE:146; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict non-empty MSSubAlgebra of U2 st the Sorts of b1 = F .:.: the Sorts of U1 & the Sorts of b2 = F .:.: the Sorts of U1 holds
b1 = b2 by MSUALG_2:9;
end;
:: deftheorem Def12 defines Image MSUALG_3:def_12_:_
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over 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 :: MSUALG_3:19
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
( F is_epimorphism U1,U2 iff Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #) )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
( F is_epimorphism U1,U2 iff Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #) )
let U1, U2 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
( F is_epimorphism U1,U2 iff Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #) )
let F be ManySortedFunction of U1,U2; ::_thesis: ( F is_homomorphism U1,U2 implies ( F is_epimorphism U1,U2 iff Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #) ) )
set FF = F .:.: the Sorts of U1;
assume A1: F is_homomorphism U1,U2 ; ::_thesis: ( F is_epimorphism U1,U2 iff Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #) )
thus ( F is_epimorphism U1,U2 implies Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #) ) ::_thesis: ( Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #) implies F is_epimorphism U1,U2 )
proof
assume F is_epimorphism U1,U2 ; ::_thesis: Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #)
then A2: F is "onto" by Def8;
now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S_holds_
(F_.:.:_the_Sorts_of_U1)_._i_=_the_Sorts_of_U2_._i
let i be set ; ::_thesis: ( i in the carrier of S implies (F .:.: the Sorts of U1) . i = the Sorts of U2 . i )
assume A3: i in the carrier of S ; ::_thesis: (F .:.: the Sorts of U1) . i = the Sorts of U2 . i
then reconsider f = F . i as Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) by PBOOLE:def_15;
A4: rng f = the Sorts of U2 . i by A2, A3, Def3;
reconsider f = f as Function ;
( (F .:.: the Sorts of U1) . i = f .: ( the Sorts of U1 . i) & dom f = the Sorts of U1 . i ) by A3, FUNCT_2:def_1, PBOOLE:def_20;
hence (F .:.: the Sorts of U1) . i = the Sorts of U2 . i by A4, RELAT_1:113; ::_thesis: verum
end;
then A5: F .:.: the Sorts of U1 = the Sorts of U2 by PBOOLE:3;
MSAlgebra(# the Sorts of U2, the Charact of U2 #) is strict MSSubAlgebra of U2 by MSUALG_2:5;
hence Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #) by A1, A5, Def12; ::_thesis: verum
end;
assume Image F = MSAlgebra(# the Sorts of U2, the Charact of U2 #) ; ::_thesis: F is_epimorphism U1,U2
then A6: F .:.: the Sorts of U1 = the Sorts of U2 by A1, Def12;
for i being set st i in the carrier of S holds
rng (F . i) = the Sorts of U2 . i
proof
let i be set ; ::_thesis: ( i in the carrier of S implies rng (F . i) = the Sorts of U2 . i )
assume i in the carrier of S ; ::_thesis: rng (F . i) = the Sorts of U2 . i
then reconsider i = i as Element of S ;
reconsider f = F . i as Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) ;
( f .: ( the Sorts of U1 . i) = the Sorts of U2 . i & dom f = the Sorts of U1 . i ) by A6, FUNCT_2:def_1, PBOOLE:def_20;
hence rng (F . i) = the Sorts of U2 . i by RELAT_1:113; ::_thesis: verum
end;
then F is "onto" by Def3;
hence F is_epimorphism U1,U2 by A1, Def8; ::_thesis: verum
end;
Lm3: for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
F is ManySortedFunction of U1,(Image F)
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
F is ManySortedFunction of U1,(Image F)
let U1, U2 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
F is ManySortedFunction of U1,(Image F)
let F be ManySortedFunction of U1,U2; ::_thesis: ( F is_homomorphism U1,U2 implies F is ManySortedFunction of U1,(Image F) )
assume A1: F is_homomorphism U1,U2 ; ::_thesis: F is ManySortedFunction of U1,(Image F)
for i being set st i in the carrier of S holds
F . i is Function of ( the Sorts of U1 . i),( the Sorts of (Image F) . i)
proof
let i be set ; ::_thesis: ( i in the carrier of S implies F . i is Function of ( the Sorts of U1 . i),( the Sorts of (Image F) . i) )
assume A2: i in the carrier of S ; ::_thesis: F . i is Function of ( the Sorts of U1 . i),( the Sorts of (Image F) . i)
then reconsider f = F . i as Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) by PBOOLE:def_15;
A3: dom f = the Sorts of U1 . i by A2, FUNCT_2:def_1;
the Sorts of (Image F) = F .:.: the Sorts of U1 by A1, Def12;
then the Sorts of (Image F) . i = f .: ( the Sorts of U1 . i) by A2, PBOOLE:def_20
.= rng f by A3, RELAT_1:113 ;
hence F . i is Function of ( the Sorts of U1 . i),( the Sorts of (Image F) . i) by A3, FUNCT_2:1; ::_thesis: verum
end;
hence F is ManySortedFunction of U1,(Image F) by PBOOLE:def_15; ::_thesis: verum
end;
theorem Th20: :: MSUALG_3:20
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U1,(Image F) st F = G & F is_homomorphism U1,U2 holds
G is_epimorphism U1, Image F
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U1,(Image F) st F = G & F is_homomorphism U1,U2 holds
G is_epimorphism U1, Image F
let U1, U2 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of U1,U2
for G being ManySortedFunction of U1,(Image F) st F = G & F is_homomorphism U1,U2 holds
G is_epimorphism U1, Image F
let F be ManySortedFunction of U1,U2; ::_thesis: for G being ManySortedFunction of U1,(Image F) st F = G & F is_homomorphism U1,U2 holds
G is_epimorphism U1, Image F
let G be ManySortedFunction of U1,(Image F); ::_thesis: ( F = G & F is_homomorphism U1,U2 implies G is_epimorphism U1, Image F )
assume that
A1: F = G and
A2: F is_homomorphism U1,U2 ; ::_thesis: G is_epimorphism U1, Image F
for o being OperSymbol of S st Args (o,U1) <> {} holds
for x being Element of Args (o,U1) holds (G . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(Image F))) . (G # x)
proof
set IF = Image F;
reconsider SIF = the Sorts of (Image F) as V2() MSSubset of U2 by MSUALG_2:def_9;
reconsider G1 = G as ManySortedFunction of U1,U2 by A1;
let o be OperSymbol of S; ::_thesis: ( Args (o,U1) <> {} implies for x being Element of Args (o,U1) holds (G . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(Image F))) . (G # x) )
assume Args (o,U1) <> {} ; ::_thesis: for x being Element of Args (o,U1) holds (G . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(Image F))) . (G # x)
let x be Element of Args (o,U1); ::_thesis: (G . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(Image F))) . (G # x)
set SIFo = SIF * (the_arity_of o);
set Uo = the Sorts of U2 * (the_arity_of o);
set ao = the_arity_of o;
A3: dom (Den (o,U2)) = Args (o,U2) by FUNCT_2:def_1;
A4: rng (the_arity_of o) c= the carrier of S by FINSEQ_1:def_4;
then rng (the_arity_of o) c= dom SIF by PARTFUN1:def_2;
then A5: dom (SIF * (the_arity_of o)) = dom (the_arity_of o) by RELAT_1:27;
rng (the_arity_of o) c= dom the Sorts of U2 by A4, PARTFUN1:def_2;
then A6: dom (SIF * (the_arity_of o)) = dom ( the Sorts of U2 * (the_arity_of o)) by A5, RELAT_1:27;
A7: for x being set st x in dom (SIF * (the_arity_of o)) holds
(SIF * (the_arity_of o)) . x c= ( the Sorts of U2 * (the_arity_of o)) . x
proof
let x be set ; ::_thesis: ( x in dom (SIF * (the_arity_of o)) implies (SIF * (the_arity_of o)) . x c= ( the Sorts of U2 * (the_arity_of o)) . x )
assume A8: x in dom (SIF * (the_arity_of o)) ; ::_thesis: (SIF * (the_arity_of o)) . x c= ( the Sorts of U2 * (the_arity_of o)) . x
then (the_arity_of o) . x in rng (the_arity_of o) by A5, FUNCT_1:def_3;
then reconsider k = (the_arity_of o) . x as Element of S by A4;
set f = F . k;
A9: dom (F . k) = the Sorts of U1 . k by FUNCT_2:def_1;
A10: rng (F . k) c= the Sorts of U2 . k by RELAT_1:def_19;
SIF = F .:.: the Sorts of U1 by A2, Def12;
then (SIF * (the_arity_of o)) . x = (F .:.: the Sorts of U1) . k by A8, FUNCT_1:12
.= (F . k) .: ( the Sorts of U1 . k) by PBOOLE:def_20
.= rng (F . k) by A9, RELAT_1:113 ;
hence (SIF * (the_arity_of o)) . x c= ( the Sorts of U2 * (the_arity_of o)) . x by A6, A8, A10, FUNCT_1:12; ::_thesis: verum
end;
A11: dom x = dom (the_arity_of o) by Th6;
A12: now__::_thesis:_for_a_being_set_st_a_in_dom_(the_arity_of_o)_holds_
(G_#_x)_._a_=_(G1_#_x)_._a
let a be set ; ::_thesis: ( a in dom (the_arity_of o) implies (G # x) . a = (G1 # x) . a )
assume A13: a in dom (the_arity_of o) ; ::_thesis: (G # x) . a = (G1 # x) . a
then reconsider n = a as Nat ;
(G # x) . n = (G . ((the_arity_of o) /. n)) . (x . n) by A11, A13, Def6;
hence (G # x) . a = (G1 # x) . a by A11, A13, Def6; ::_thesis: verum
end;
( dom (G # x) = dom (the_arity_of o) & dom (G1 # x) = dom (the_arity_of o) ) by Th6;
then G # x = G1 # x by A12, FUNCT_1:2;
then A14: (G . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U2)) . (G # x) by A1, A2, Def7;
SIF is opers_closed by MSUALG_2:def_9;
then A15: SIF is_closed_on o by MSUALG_2:def_6;
( Args (o,(Image F)) = product (SIF * (the_arity_of o)) & Args (o,U2) = product ( the Sorts of U2 * (the_arity_of o)) ) by PRALG_2:3;
then Args (o,(Image F)) c= Args (o,U2) by A6, A7, CARD_3:27;
then G # x in dom (Den (o,U2)) by A3, TARSKI:def_3;
then A16: ( ((SIF #) * the Arity of S) . o = Args (o,(Image F)) & G # x in (dom (Den (o,U2))) /\ (Args (o,(Image F))) ) by MSUALG_1:def_4, XBOOLE_0:def_4;
the Charact of (Image F) = Opers (U2,SIF) by MSUALG_2:def_9;
then Den (o,(Image F)) = (Opers (U2,SIF)) . o by MSUALG_1:def_6
.= o /. SIF by MSUALG_2:def_8
.= (Den (o,U2)) | (((SIF #) * the Arity of S) . o) by A15, MSUALG_2:def_7 ;
hence (G . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,(Image F))) . (G # x) by A14, A16, FUNCT_1:48; ::_thesis: verum
end;
then A17: G is_homomorphism U1, Image F by Def7;
for i being set st i in the carrier of S holds
rng (G . i) = the Sorts of (Image F) . i
proof
let i be set ; ::_thesis: ( i in the carrier of S implies rng (G . i) = the Sorts of (Image F) . i )
assume i in the carrier of S ; ::_thesis: rng (G . i) = the Sorts of (Image F) . i
then reconsider i = i as Element of S ;
set g = G . i;
the Sorts of (Image F) = G .:.: the Sorts of U1 by A1, A2, Def12;
then A18: the Sorts of (Image F) . i = (G . i) .: ( the Sorts of U1 . i) by PBOOLE:def_20;
dom (G . i) = the Sorts of U1 . i by FUNCT_2:def_1;
hence rng (G . i) = the Sorts of (Image F) . i by A18, RELAT_1:113; ::_thesis: verum
end;
then G is "onto" by Def3;
hence G is_epimorphism U1, Image F by A17, Def8; ::_thesis: verum
end;
theorem :: MSUALG_3:21
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
ex G being ManySortedFunction of U1,(Image F) st
( F = G & G is_epimorphism U1, Image F )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
ex G being ManySortedFunction of U1,(Image F) st
( F = G & G is_epimorphism U1, Image F )
let U1, U2 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
ex G being ManySortedFunction of U1,(Image F) st
( F = G & G is_epimorphism U1, Image F )
let F be ManySortedFunction of U1,U2; ::_thesis: ( F is_homomorphism U1,U2 implies ex G being ManySortedFunction of U1,(Image F) st
( F = G & G is_epimorphism U1, Image F ) )
assume A1: F is_homomorphism U1,U2 ; ::_thesis: ex G being ManySortedFunction of U1,(Image F) st
( F = G & G is_epimorphism U1, Image F )
then reconsider G = F as ManySortedFunction of U1,(Image F) by Lm3;
take G ; ::_thesis: ( F = G & G is_epimorphism U1, Image F )
thus ( F = G & G is_epimorphism U1, Image F ) by A1, Th20; ::_thesis: verum
end;
Lm4: for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over 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
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2 being non-empty MSAlgebra over 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
let U1, U2 be non-empty MSAlgebra over S; ::_thesis: 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
let U3 be non-empty MSSubAlgebra of U2; ::_thesis: 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
let F be ManySortedFunction of U1,U2; ::_thesis: for G being ManySortedFunction of U1,U3 st F = G & G is_homomorphism U1,U3 holds
F is_homomorphism U1,U2
let G be ManySortedFunction of U1,U3; ::_thesis: ( F = G & G is_homomorphism U1,U3 implies F is_homomorphism U1,U2 )
assume that
A1: F = G and
A2: G is_homomorphism U1,U3 ; ::_thesis: F is_homomorphism U1,U2
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)
proof
reconsider S3 = the Sorts of U3 as V2() MSSubset of U2 by MSUALG_2:def_9;
let o be OperSymbol of S; ::_thesis: ( Args (o,U1) <> {} implies for x being Element of Args (o,U1) holds (F . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U2)) . (F # x) )
assume Args (o,U1) <> {} ; ::_thesis: for x being Element of Args (o,U1) holds (F . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U2)) . (F # x)
let x be Element of Args (o,U1); ::_thesis: (F . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U2)) . (F # x)
for i being set st i in the carrier of S holds
G . i is Function of ( the Sorts of U1 . i),( the Sorts of U2 . i)
proof
reconsider S3 = the Sorts of U3 as V2() MSSubset of U2 by MSUALG_2:def_9;
let i be set ; ::_thesis: ( i in the carrier of S implies G . i is Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) )
assume A3: i in the carrier of S ; ::_thesis: G . i is Function of ( the Sorts of U1 . i),( the Sorts of U2 . i)
then reconsider g = G . i as Function of ( the Sorts of U1 . i),( the Sorts of U3 . i) by PBOOLE:def_15;
the Sorts of U3 is MSSubset of U2 by MSUALG_2:def_9;
then the Sorts of U3 c= the Sorts of U2 by PBOOLE:def_18;
then S3 . i c= the Sorts of U2 . i by A3, PBOOLE:def_2;
then g is Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) by A3, FUNCT_2:7;
hence G . i is Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) ; ::_thesis: verum
end;
then reconsider G1 = G as ManySortedFunction of U1,U2 by PBOOLE:def_15;
S3 is opers_closed by MSUALG_2:def_9;
then A4: S3 is_closed_on o by MSUALG_2:def_6;
the Charact of U3 = Opers (U2,S3) by MSUALG_2:def_9;
then A5: Den (o,U3) = (Opers (U2,S3)) . o by MSUALG_1:def_6
.= o /. S3 by MSUALG_2:def_8
.= (Den (o,U2)) | (((S3 #) * the Arity of S) . o) by A4, MSUALG_2:def_7 ;
A6: dom x = dom (the_arity_of o) by Th6;
A7: now__::_thesis:_for_a_being_set_st_a_in_dom_(the_arity_of_o)_holds_
(G_#_x)_._a_=_(G1_#_x)_._a
let a be set ; ::_thesis: ( a in dom (the_arity_of o) implies (G # x) . a = (G1 # x) . a )
assume A8: a in dom (the_arity_of o) ; ::_thesis: (G # x) . a = (G1 # x) . a
then reconsider n = a as Nat ;
(G # x) . n = (G . ((the_arity_of o) /. n)) . (x . n) by A6, A8, Def6;
hence (G # x) . a = (G1 # x) . a by A6, A8, Def6; ::_thesis: verum
end;
( dom (G # x) = dom (the_arity_of o) & dom (G1 # x) = dom (the_arity_of o) ) by Th6;
then A9: G # x = G1 # x by A7, FUNCT_1:2;
dom (Den (o,U2)) = Args (o,U2) by FUNCT_2:def_1;
then A10: ( ((S3 #) * the Arity of S) . o = Args (o,U3) & F # x in (dom (Den (o,U2))) /\ (Args (o,U3)) ) by A1, A9, MSUALG_1:def_4, XBOOLE_0:def_4;
(F . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U3)) . (F # x) by A1, A2, A9, Def7;
hence (F . (the_result_sort_of o)) . ((Den (o,U1)) . x) = (Den (o,U2)) . (F # x) by A5, A10, FUNCT_1:48; ::_thesis: verum
end;
hence F is_homomorphism U1,U2 by Def7; ::_thesis: verum
end;
theorem Th22: :: MSUALG_3:22
for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for U2 being non-empty MSSubAlgebra of U1
for G being ManySortedFunction of U2,U1 st G = id the Sorts of U2 holds
G is_monomorphism U2,U1
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U1 being non-empty MSAlgebra over S
for U2 being non-empty MSSubAlgebra of U1
for G being ManySortedFunction of U2,U1 st G = id the Sorts of U2 holds
G is_monomorphism U2,U1
let U1 be non-empty MSAlgebra over S; ::_thesis: for U2 being non-empty MSSubAlgebra of U1
for G being ManySortedFunction of U2,U1 st G = id the Sorts of U2 holds
G is_monomorphism U2,U1
let U2 be non-empty MSSubAlgebra of U1; ::_thesis: for G being ManySortedFunction of U2,U1 st G = id the Sorts of U2 holds
G is_monomorphism U2,U1
let G be ManySortedFunction of U2,U1; ::_thesis: ( G = id the Sorts of U2 implies G is_monomorphism U2,U1 )
set F = id the Sorts of U2;
assume A1: G = id the Sorts of U2 ; ::_thesis: G is_monomorphism U2,U1
for i being set st i in the carrier of S holds
G . i is one-to-one
proof
let i be set ; ::_thesis: ( i in the carrier of S implies G . i is one-to-one )
assume A2: i in the carrier of S ; ::_thesis: G . i is one-to-one
then reconsider f = (id the Sorts of U2) . i as Function of ( the Sorts of U2 . i),( the Sorts of U2 . i) by PBOOLE:def_15;
f = id ( the Sorts of U2 . i) by A2, Def1;
hence G . i is one-to-one by A1; ::_thesis: verum
end;
then A3: G is "1-1" by Th1;
G is_homomorphism U2,U1 by A1, Lm4, Th9;
hence G is_monomorphism U2,U1 by A3, Def9; ::_thesis: verum
end;
theorem :: MSUALG_3:23
for S being non empty non void ManySortedSign
for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
ex F1 being ManySortedFunction of U1,(Image F) ex F2 being ManySortedFunction of (Image F),U2 st
( F1 is_epimorphism U1, Image F & F2 is_monomorphism Image F,U2 & F = F2 ** F1 )
proof
let S be non empty non void ManySortedSign ; ::_thesis: for U1, U2 being non-empty MSAlgebra over S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
ex F1 being ManySortedFunction of U1,(Image F) ex F2 being ManySortedFunction of (Image F),U2 st
( F1 is_epimorphism U1, Image F & F2 is_monomorphism Image F,U2 & F = F2 ** F1 )
let U1, U2 be non-empty MSAlgebra over S; ::_thesis: for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 holds
ex F1 being ManySortedFunction of U1,(Image F) ex F2 being ManySortedFunction of (Image F),U2 st
( F1 is_epimorphism U1, Image F & F2 is_monomorphism Image F,U2 & F = F2 ** F1 )
let F be ManySortedFunction of U1,U2; ::_thesis: ( F is_homomorphism U1,U2 implies ex F1 being ManySortedFunction of U1,(Image F) ex F2 being ManySortedFunction of (Image F),U2 st
( F1 is_epimorphism U1, Image F & F2 is_monomorphism Image F,U2 & F = F2 ** F1 ) )
assume A1: F is_homomorphism U1,U2 ; ::_thesis: ex F1 being ManySortedFunction of U1,(Image F) ex F2 being ManySortedFunction of (Image F),U2 st
( F1 is_epimorphism U1, Image F & F2 is_monomorphism Image F,U2 & F = F2 ** F1 )
then reconsider F1 = F as ManySortedFunction of U1,(Image F) by Lm3;
for H being ManySortedFunction of (Image F),(Image F) holds H is ManySortedFunction of (Image F),U2
proof
let H be ManySortedFunction of (Image F),(Image F); ::_thesis: H is ManySortedFunction of (Image F),U2
for i being set st i in the carrier of S holds
H . i is Function of ( the Sorts of (Image F) . i),( the Sorts of U2 . i)
proof
let i be set ; ::_thesis: ( i in the carrier of S implies H . i is Function of ( the Sorts of (Image F) . i),( the Sorts of U2 . i) )
assume A2: i in the carrier of S ; ::_thesis: H . i is Function of ( the Sorts of (Image F) . i),( the Sorts of U2 . i)
then reconsider f = F . i as Function of ( the Sorts of U1 . i),( the Sorts of U2 . i) by PBOOLE:def_15;
A3: dom f = the Sorts of U1 . i by A2, FUNCT_2:def_1;
reconsider h = H . i as Function of ( the Sorts of (Image F) . i),( the Sorts of (Image F) . i) by A2, PBOOLE:def_15;
A4: rng f c= the Sorts of U2 . i by RELAT_1:def_19;
the Sorts of (Image F) = F .:.: the Sorts of U1 by A1, Def12;
then the Sorts of (Image F) . i = f .: ( the Sorts of U1 . i) by A2, PBOOLE:def_20
.= rng f by A3, RELAT_1:113 ;
then h is Function of ( the Sorts of (Image F) . i),( the Sorts of U2 . i) by A4, FUNCT_2:7;
hence H . i is Function of ( the Sorts of (Image F) . i),( the Sorts of U2 . i) ; ::_thesis: verum
end;
hence H is ManySortedFunction of (Image F),U2 by PBOOLE:def_15; ::_thesis: verum
end;
then reconsider F2 = id the Sorts of (Image F) as ManySortedFunction of (Image F),U2 ;
take F1 ; ::_thesis: ex F2 being ManySortedFunction of (Image F),U2 st
( F1 is_epimorphism U1, Image F & F2 is_monomorphism Image F,U2 & F = F2 ** F1 )
take F2 ; ::_thesis: ( F1 is_epimorphism U1, Image F & F2 is_monomorphism Image F,U2 & F = F2 ** F1 )
thus F1 is_epimorphism U1, Image F by A1, Th20; ::_thesis: ( F2 is_monomorphism Image F,U2 & F = F2 ** F1 )
thus F2 is_monomorphism Image F,U2 by Th22; ::_thesis: F = F2 ** F1
thus F = F2 ** F1 by Th4; ::_thesis: verum
end;
theorem :: MSUALG_3:24
for S being non empty non void ManySortedSign
for U1, U2 being MSAlgebra over 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 iff for n being Nat st n in dom f holds
u . n = (F . ((the_arity_of o) /. n)) . (f . n) ) by Lm1;