set T = the non-empty disjoint_valued trivial MSAlgebra over S;
set h = the ManySortedFunction of A, the non-empty disjoint_valued trivial MSAlgebra over S;
reconsider T0 = the non-empty disjoint_valued trivial MSAlgebra over S as MSAlgebra over S ;
T0 is A -Image

proof

take the non-empty disjoint_valued trivial MSAlgebra over S ; :: according to MSAFREE4:def 4 :: thesis: ex h being ManySortedFunction of A, the non-empty disjoint_valued trivial MSAlgebra over S st
( h is_homomorphism A, the non-empty disjoint_valued trivial MSAlgebra over S & MSAlgebra(# the Sorts of T0, the Charact of T0 #) = Image h )
take the ManySortedFunction of A, the non-empty disjoint_valued trivial MSAlgebra over S ; :: thesis: ( the ManySortedFunction of A, the non-empty disjoint_valued trivial MSAlgebra over S is_homomorphism A, the non-empty disjoint_valued trivial MSAlgebra over S & MSAlgebra(# the Sorts of T0, the Charact of T0 #) = Image the ManySortedFunction of A, the non-empty disjoint_valued trivial MSAlgebra over S )
thus the ManySortedFunction of A, the non-empty disjoint_valued trivial MSAlgebra over S is_homomorphism A, the non-empty disjoint_valued trivial MSAlgebra over S by Th33; :: thesis: MSAlgebra(# the Sorts of T0, the Charact of T0 #) = Image the ManySortedFunction of A, the non-empty disjoint_valued trivial MSAlgebra over S
thus MSAlgebra(# the Sorts of T0, the Charact of T0 #) = Image the ManySortedFunction of A, the non-empty disjoint_valued trivial MSAlgebra over S by Th34; :: thesis: verum

end;

hence ex b₁ being image of A st
( b₁ is disjoint_valued & b₁ is trivial ) ; :: thesis: verum