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

G is_homomorphism U2,U1 by A1, Lm4, Th9;

hence G is_monomorphism U2,U1 by A3; :: thesis: verum

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

then A3:
G is "1-1"
by Th1;
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;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

G is_homomorphism U2,U1 by A1, Lm4, Th9;

hence G is_monomorphism U2,U1 by A3; :: thesis: verum