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
;
MSAFREE4:def 4 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
;
( 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;
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;
verum
end;
hence
ex b1 being image of A st
( b1 is disjoint_valued & b1 is trivial )
; verum