take C = Image (id the Sorts of A); :: thesis: C is A -Image
take A ; :: according to MSAFREE4:def 4 :: thesis: ex h being ManySortedFunction of A,A st
( h is_homomorphism A,A & MSAlgebra(# the Sorts of C, the Charact of C #) = Image h )
take h = id the Sorts of A; :: thesis: ( h is_homomorphism A,A & MSAlgebra(# the Sorts of C, the Charact of C #) = Image h )
thus h is_homomorphism A,A by MSUALG_3:9; :: thesis: MSAlgebra(# the Sorts of C, the Charact of C #) = Image h
thus MSAlgebra(# the Sorts of C, the Charact of C #) = Image h ; :: thesis: verum