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