:: by Ma{\l}gorzata Korolkiewicz

::

:: Received April 25, 1994

:: Copyright (c) 1994-2021 Association of Mizar Users

:: PRELIMINARIES - MANY SORTED FUNCTIONS

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 func F . i -> Function of (A . i),(B . i);

coherence

F . i is Function of (A . i),(B . i) by PBOOLE:def 15;

end;
let A, B be ManySortedSet of I;

let F be ManySortedFunction of A,B;

let i be Element of I;

:: original: .

redefine func F . i -> Function of (A . i),(B . i);

coherence

F . i is Function of (A . i),(B . i) by PBOOLE:def 15;

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;
let U1, U2 be MSAlgebra over S;

mode ManySortedFunction of U1,U2 is ManySortedFunction of the Sorts of U1, the Sorts of U2;

definition

let I be set ;

let A be ManySortedSet of I;

ex b_{1} being ManySortedFunction of A,A st

for i being set st i in I holds

b_{1} . i = id (A . i)

for b_{1}, b_{2} being ManySortedFunction of A,A st ( for i being set st i in I holds

b_{1} . i = id (A . i) ) & ( for i being set st i in I holds

b_{2} . i = id (A . i) ) holds

b_{1} = b_{2}

end;
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 for i being set st i in I holds

it . i = id (A . i);

ex b

for i being set st i in I holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def1 defines id MSUALG_3:def 1 :

for I being set

for A being ManySortedSet of I

for b_{3} being ManySortedFunction of A,A holds

( b_{3} = id A iff for i being set st i in I holds

b_{3} . i = id (A . i) );

for I being set

for A being ManySortedSet of I

for b

( b

b

definition

let IT be Function;

end;
attr IT is "1-1" means :: 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 ;

for i being set

for f being Function st i in dom IT & IT . i = f holds

f is one-to-one ;

:: deftheorem 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 );

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
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 )

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 end;

:: deftheorem 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 );

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) ) )

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 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 func G ** F -> ManySortedFunction of A,C;

coherence

G ** F is ManySortedFunction of A,C

end;
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 func G ** F -> ManySortedFunction of A,C;

coherence

G ** F is ManySortedFunction of A,C

proof 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

for A, B being ManySortedSet of I

for F being ManySortedFunction of A,B holds F ** (id A) = F

proof 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

for A, B being ManySortedSet of I

for F being ManySortedFunction of A,B holds (id B) ** F = F

proof 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" ;

ex b_{1} being ManySortedFunction of B,A st

for i being set st i in I holds

b_{1} . i = (F . i) "

for b_{1}, b_{2} being ManySortedFunction of B,A st ( for i being set st i in I holds

b_{1} . i = (F . i) " ) & ( for i being set st i in I holds

b_{2} . i = (F . i) " ) holds

b_{1} = b_{2}

end;
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" ;

func F "" -> ManySortedFunction of B,A means :Def4: :: MSUALG_3:def 4

for i being set st i in I holds

it . i = (F . i) " ;

existence for i being set st i in I holds

it . i = (F . i) " ;

ex b

for i being set st i in I holds

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{5} being ManySortedFunction of B,A holds

( b_{5} = F "" iff for i being set st i in I holds

b_{5} . i = (F . i) " );

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 b

( b

b

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 )

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 end;

registration

let S be non empty non void ManySortedSign ;

let U1 be non-empty MSAlgebra over S;

let o be OperSymbol of S;

coherence

Args (o,U1) is functional

end;
let U1 be non-empty MSAlgebra over S;

let o be OperSymbol of S;

coherence

Args (o,U1) is functional

proof end;

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 ) )

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 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) <> {} ;

(Frege (F * (the_arity_of o))) . x is Element of Args (o,U2)

;

end;
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) <> {} ;

func F # 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;

(Frege (F * (the_arity_of o))) . x is Element of Args (o,U2)

proof end;

correctness ;

:: 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;

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 f = x & 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 ) )

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 f = x & 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 f = x & 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 f = x & 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 f = x & 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 f = x & 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 f = x & 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: ( f = x & 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: f = x 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;

A6: F # x = (Frege (F * (the_arity_of o))) . x by A2, A3, Def5;

A7: dom ( the Sorts of U1 * (the_arity_of o)) = dom (F * (the_arity_of o))

then A12: dom u = dom ( the Sorts of U2 * (the_arity_of o)) by A3, CARD_3:9;

A13: Args (o,U1) = product ( the Sorts of U1 * (the_arity_of o)) by PRALG_2:3;

A14: dom f = dom (the_arity_of o) by A1, A2, Th6;

rng (the_arity_of o) c= dom the Sorts of U2 by A4, PARTFUN1:def 2;

then A15: dom u = dom (the_arity_of o) by A12, RELAT_1:27;

set tao = the_arity_of o;

then reconsider g = F # x as Function ;

A23: rng (the_arity_of o) c= dom F by A4, PARTFUN1:def 2;

assume A24: for n being Nat st n in dom f holds

u . n = (F . ((the_arity_of o) /. n)) . (f . n) ; :: thesis: u = F # x

F # x = (F * (the_arity_of o)) .. f by A1, A2, A13, A18, A6, PRALG_2:def 2;

then dom g = (dom (F * (the_arity_of o))) /\ (dom f) by PRALG_1:def 19

.= (dom (the_arity_of o)) /\ (dom f) by A23, RELAT_1:27 ;

hence u = F # x by A14, A15, A25, FUNCT_1:2; :: thesis: verum

end;
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 f = x & 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 f = x & 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 f = x & 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 f = x & 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 f = x & 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: ( f = x & 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: f = x 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;

A6: F # x = (Frege (F * (the_arity_of o))) . x by A2, A3, Def5;

A7: dom ( the Sorts of U1 * (the_arity_of o)) = dom (F * (the_arity_of o))

proof

assume e in dom (F * (the_arity_of o)) ; :: thesis: e in dom ( the Sorts of U1 * (the_arity_of o))

then A10: 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 A10, 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 A10, FUNCT_1:11; :: thesis: verum

end;

A11:
Args (o,U2) = product ( the Sorts of U2 * (the_arity_of o))
by PRALG_2:3;
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: dom (F * (the_arity_of o)) c= dom ( the Sorts of U1 * (the_arity_of o))

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in dom (F * (the_arity_of o)) or e in dom ( the Sorts of U1 * (the_arity_of o)) )
let e be object ; :: thesis: ( e in dom ( the Sorts of U1 * (the_arity_of o)) implies e in dom (F * (the_arity_of o)) )

assume A8: e in dom ( the Sorts of U1 * (the_arity_of o)) ; :: thesis: e in dom (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 A9: (the_arity_of o) . e in dom F by PARTFUN1:def 2;

e in dom (the_arity_of o) by A8, FUNCT_1:11;

then e in dom (F * (the_arity_of o)) by A9, FUNCT_1:11;

hence e in dom (F * (the_arity_of o)) ; :: thesis: verum

end;
assume A8: e in dom ( the Sorts of U1 * (the_arity_of o)) ; :: thesis: e in dom (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 A9: (the_arity_of o) . e in dom F by PARTFUN1:def 2;

e in dom (the_arity_of o) by A8, FUNCT_1:11;

then e in dom (F * (the_arity_of o)) by A9, FUNCT_1:11;

hence e in dom (F * (the_arity_of o)) ; :: thesis: verum

assume e in dom (F * (the_arity_of o)) ; :: thesis: e in dom ( the Sorts of U1 * (the_arity_of o))

then A10: 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 A10, 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 A10, FUNCT_1:11; :: thesis: verum

then A12: dom u = dom ( the Sorts of U2 * (the_arity_of o)) by A3, CARD_3:9;

A13: Args (o,U1) = product ( the Sorts of U1 * (the_arity_of o)) by PRALG_2:3;

A14: dom f = dom (the_arity_of o) by A1, A2, Th6;

rng (the_arity_of o) c= dom the Sorts of U2 by A4, PARTFUN1:def 2;

then A15: dom u = dom (the_arity_of o) by A12, RELAT_1:27;

set tao = the_arity_of o;

now :: thesis: for e being object st e in dom (F * (the_arity_of o)) holds

( the Sorts of U1 * (the_arity_of o)) . e = proj1 ((F * (the_arity_of o)) . e)

then A18:
the Sorts of U1 * (the_arity_of o) = doms (F * (the_arity_of o))
by A7, FUNCT_6:def 2;( the Sorts of U1 * (the_arity_of o)) . e = proj1 ((F * (the_arity_of o)) . e)

let e be object ; :: thesis: ( e in dom (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 dom (F * (the_arity_of o)) ; :: thesis: ( the Sorts of U1 * (the_arity_of o)) . e = proj1 ((F * (the_arity_of o)) . e)

then A16: 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 A12, A15, A16, FUNCT_1:def 3;

then A17: ( the Sorts of U2 * (the_arity_of o)) . e <> {} by A3, A11, 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 A16, FUNCT_1:13;

hence ( the Sorts of U1 * (the_arity_of o)) . e = dom Foe by A17, FUNCT_2:def 1

.= proj1 ((F * (the_arity_of o)) . e) by A16, FUNCT_1:13 ;

:: thesis: verum

end;
assume e in dom (F * (the_arity_of o)) ; :: thesis: ( the Sorts of U1 * (the_arity_of o)) . e = proj1 ((F * (the_arity_of o)) . e)

then A16: 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 A12, A15, A16, FUNCT_1:def 3;

then A17: ( the Sorts of U2 * (the_arity_of o)) . e <> {} by A3, A11, 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 A16, FUNCT_1:13;

hence ( the Sorts of U1 * (the_arity_of o)) . e = dom Foe by A17, FUNCT_2:def 1

.= proj1 ((F * (the_arity_of o)) . e) by A16, FUNCT_1:13 ;

:: thesis: verum

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 )

F # x is Element of product ( the Sorts of U2 * (the_arity_of o))
by PRALG_2:3;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 A19: 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 A20: 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 A14, FINSEQ_2:11;

then (the_arity_of o) . n in dom F by PARTFUN1:def 2;

then A21: n in dom (F * (the_arity_of o)) by A14, A20, FUNCT_1:11;

then n in (dom (F * (the_arity_of o))) /\ (dom f) by A20, XBOOLE_0:def 4;

then a21: n in dom ((F * (the_arity_of o)) .. f) by PRALG_1:def 19;

A22: (F * (the_arity_of o)) . n = F . ((the_arity_of o) . n) by FUNCT_1:12, A21

.= F . ((the_arity_of o) /. n) by A14, A20, PARTFUN1:def 6 ;

thus u . n = ((F * (the_arity_of o)) .. f) . n by A1, A2, A13, A18, A19, PRALG_2:def 2

.= (F . ((the_arity_of o) /. n)) . (f . n) by A22, PRALG_1:def 19, a21 ; :: thesis: verum

end;
u . n = (F . ((the_arity_of o) /. n)) . (f . n)

then A19: 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 A20: 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 A14, FINSEQ_2:11;

then (the_arity_of o) . n in dom F by PARTFUN1:def 2;

then A21: n in dom (F * (the_arity_of o)) by A14, A20, FUNCT_1:11;

then n in (dom (F * (the_arity_of o))) /\ (dom f) by A20, XBOOLE_0:def 4;

then a21: n in dom ((F * (the_arity_of o)) .. f) by PRALG_1:def 19;

A22: (F * (the_arity_of o)) . n = F . ((the_arity_of o) . n) by FUNCT_1:12, A21

.= F . ((the_arity_of o) /. n) by A14, A20, PARTFUN1:def 6 ;

thus u . n = ((F * (the_arity_of o)) .. f) . n by A1, A2, A13, A18, A19, PRALG_2:def 2

.= (F . ((the_arity_of o) /. n)) . (f . n) by A22, PRALG_1:def 19, a21 ; :: thesis: verum

then reconsider g = F # x as Function ;

A23: rng (the_arity_of o) c= dom F by A4, PARTFUN1:def 2;

assume A24: for n being Nat st n in dom f holds

u . n = (F . ((the_arity_of o) /. n)) . (f . n) ; :: thesis: u = F # x

A25: now :: thesis: for e being object st e in dom f holds

u . e = g . e

dom f = dom (the_arity_of o)
by A1, A2, Th6;u . e = g . e

let e be object ; :: thesis: ( e in dom f implies u . e = g . e )

assume A26: e in dom f ; :: thesis: u . e = g . e

then reconsider n = e as Nat by A14;

(the_arity_of o) . n in the carrier of S by A14, A26, FINSEQ_2:11;

then (the_arity_of o) . n in dom F by PARTFUN1:def 2;

then A27: n in dom (F * (the_arity_of o)) by A14, A26, FUNCT_1:11;

then n in (dom (F * (the_arity_of o))) /\ (dom f) by A26, XBOOLE_0:def 4;

then a27: n in dom ((F * (the_arity_of o)) .. f) by PRALG_1:def 19;

A28: (F * (the_arity_of o)) . n = F . ((the_arity_of o) . n) by FUNCT_1:12, A27

.= F . ((the_arity_of o) /. n) by A14, A26, PARTFUN1:def 6 ;

thus u . e = (F . ((the_arity_of o) /. n)) . (f . n) by A24, A26

.= ((F * (the_arity_of o)) .. f) . n by a27, A28, PRALG_1:def 19

.= g . e by A1, A2, A13, A18, A6, PRALG_2:def 2 ; :: thesis: verum

end;
assume A26: e in dom f ; :: thesis: u . e = g . e

then reconsider n = e as Nat by A14;

(the_arity_of o) . n in the carrier of S by A14, A26, FINSEQ_2:11;

then (the_arity_of o) . n in dom F by PARTFUN1:def 2;

then A27: n in dom (F * (the_arity_of o)) by A14, A26, FUNCT_1:11;

then n in (dom (F * (the_arity_of o))) /\ (dom f) by A26, XBOOLE_0:def 4;

then a27: n in dom ((F * (the_arity_of o)) .. f) by PRALG_1:def 19;

A28: (F * (the_arity_of o)) . n = F . ((the_arity_of o) . n) by FUNCT_1:12, A27

.= F . ((the_arity_of o) /. n) by A14, A26, PARTFUN1:def 6 ;

thus u . e = (F . ((the_arity_of o) /. n)) . (f . n) by A24, A26

.= ((F * (the_arity_of o)) .. f) . n by a27, A28, PRALG_1:def 19

.= g . e by A1, A2, A13, A18, A6, PRALG_2:def 2 ; :: thesis: verum

F # x = (F * (the_arity_of o)) .. f by A1, A2, A13, A18, A6, PRALG_2:def 2;

then dom g = (dom (F * (the_arity_of o))) /\ (dom f) by PRALG_1:def 19

.= (dom (the_arity_of o)) /\ (dom f) by A23, RELAT_1:27 ;

hence u = F # x by A14, A15, A25, FUNCT_1:2; :: thesis: verum

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);

for b_{1} being Element of Args (o,U2) holds

( b_{1} = F # x iff for n being Nat st n in dom x holds

b_{1} . n = (F . ((the_arity_of o) /. n)) . (x . n) )
by Lm1;

end;
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 n being Nat st n in dom x holds

it . n = (F . ((the_arity_of o) /. n)) . (x . n);

for b

( b

b

:: 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 b_{7} being Element of Args (o,U2) holds

( b_{7} = F # x iff for n being Nat st n in dom x holds

b_{7} . n = (F . ((the_arity_of o) /. n)) . (x . n) );

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 b

( b

b

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

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 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)

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 end;

definition

let S be non empty non void ManySortedSign ;

let U1, U2 be MSAlgebra over S;

let F be ManySortedFunction of U1,U2;

end;
let U1, U2 be MSAlgebra over S;

let F be ManySortedFunction of U1,U2;

pred F is_homomorphism U1,U2 means :: 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);

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);

:: deftheorem 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) );

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

for U1 being MSAlgebra over S holds id the Sorts of U1 is_homomorphism U1,U1

proof 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

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 end;

definition

let S be non empty non void ManySortedSign ;

let U1, U2 be MSAlgebra over S;

let F be ManySortedFunction of U1,U2;

end;
let U1, U2 be MSAlgebra over S;

let F be ManySortedFunction of U1,U2;

:: deftheorem 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" ) );

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

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 end;

definition

let S be non empty non void ManySortedSign ;

let U1, U2 be MSAlgebra over S;

let F be ManySortedFunction of U1,U2;

end;
let U1, U2 be MSAlgebra over S;

let F be ManySortedFunction of U1,U2;

:: deftheorem 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" ) );

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

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 end;

definition

let S be non empty non void ManySortedSign ;

let U1, U2 be MSAlgebra over S;

let F be ManySortedFunction of U1,U2;

end;
let U1, U2 be MSAlgebra over S;

let F be ManySortedFunction of U1,U2;

pred F is_isomorphism U1,U2 means :: MSUALG_3:def 10

( F is_epimorphism U1,U2 & F is_monomorphism U1,U2 );

( F is_epimorphism U1,U2 & F is_monomorphism U1,U2 );

:: deftheorem 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 ) );

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" ) )

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 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 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

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 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 by Th11, Th12;

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 by Th11, Th12;

definition

let S be non empty non void ManySortedSign ;

let U1, U2 be MSAlgebra over S;

end;
let U1, U2 be MSAlgebra over S;

pred U1,U2 are_isomorphic means :: MSUALG_3:def 11

ex F being ManySortedFunction of U1,U2 st F is_isomorphism U1,U2;

ex F being ManySortedFunction of U1,U2 st F is_isomorphism U1,U2;

:: deftheorem 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 );

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 )

for U1 being MSAlgebra over S holds

( id the Sorts of U1 is_isomorphism U1,U1 & U1,U1 are_isomorphic )

proof end;

definition

let S be non empty non void ManySortedSign ;

let U1, U2 be MSAlgebra over S;

:: original: are_isomorphic

redefine pred U1,U2 are_isomorphic ;

reflexivity

for U1 being MSAlgebra over S holds (S,b_{1},b_{1})
by Th16;

end;
let U1, U2 be MSAlgebra over S;

:: original: are_isomorphic

redefine pred U1,U2 are_isomorphic ;

reflexivity

for U1 being MSAlgebra over S holds (S,b

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

for U1, U2 being non-empty MSAlgebra over S st U1,U2 are_isomorphic holds

U2,U1 are_isomorphic

proof 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

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 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 ;

ex b_{1} being strict non-empty MSSubAlgebra of U2 st the Sorts of b_{1} = F .:.: the Sorts of U1

for b_{1}, b_{2} being strict non-empty MSSubAlgebra of U2 st the Sorts of b_{1} = F .:.: the Sorts of U1 & the Sorts of b_{2} = F .:.: the Sorts of U1 holds

b_{1} = b_{2}
by MSUALG_2:9;

end;
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 the Sorts of it = F .:.: the Sorts of U1;

ex b

proof end;

uniqueness for b

b

:: 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 b_{5} being strict non-empty MSSubAlgebra of U2 holds

( b_{5} = Image F iff the Sorts of b_{5} = F .:.: the Sorts of U1 );

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 b

( b

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 #) )

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 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 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

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 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 )

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 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 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

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 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 )

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 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;

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;