let S be non empty non void ManySortedSign ; :: thesis: for A being non-empty MSAlgebra over S holds A is image of A
let A be non-empty MSAlgebra over S; :: thesis: A is image of A
A is A -Image
proof
now :: thesis: ex B being non-empty MSAlgebra over S ex h being ManySortedFunction of the Sorts of A, the Sorts of B st
( h is_homomorphism A,B & MSAlgebra(# the Sorts of A, the Charact of A #) = Image h )
take B = A; :: thesis: ex h being ManySortedFunction of the Sorts of A, the Sorts of B st
( h is_homomorphism A,B & MSAlgebra(# the Sorts of A, the Charact of A #) = Image h )
reconsider h = id the Sorts of A as ManySortedFunction of the Sorts of A, the Sorts of B ;
take h = h; :: thesis: ( h is_homomorphism A,B & MSAlgebra(# the Sorts of A, the Charact of A #) = Image h )
thus h is_homomorphism A,B by MSUALG_3:9; :: thesis: MSAlgebra(# the Sorts of A, the Charact of A #) = Image h
thus MSAlgebra(# the Sorts of A, the Charact of A #) = Image h by Th5; :: thesis: verum
end;
hence A is A -Image by MSAFREE4:def 4; :: thesis: verum
end;
hence A is image of A ; :: thesis: verum