let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra over S st ex X being ManySortedSet of the carrier of S st the Sorts of A = {X} holds
A, Trivial_Algebra S are_isomorphic
let A be MSAlgebra over S; :: thesis: ( ex X being ManySortedSet of the carrier of S st the Sorts of A = {X} implies A, Trivial_Algebra S are_isomorphic )
assume A1: ex X being ManySortedSet of the carrier of S st the Sorts of A = {X} ; :: thesis: A, Trivial_Algebra S are_isomorphic
set I = the carrier of S;
set SB = the Sorts of A;
set ST = the Sorts of (Trivial_Algebra S);
consider X being ManySortedSet of the carrier of S such that
A2: the Sorts of A = {X} by A1;
set F = the ManySortedFunction of the Sorts of A, the Sorts of (Trivial_Algebra S);
reconsider F1 = the ManySortedFunction of the Sorts of A, the Sorts of (Trivial_Algebra S) as ManySortedFunction of {X}, the Sorts of (Trivial_Algebra S) by A2;
take the ManySortedFunction of the Sorts of A, the Sorts of (Trivial_Algebra S) ; :: according to MSUALG_3:def 11 :: thesis: the ManySortedFunction of the Sorts of A, the Sorts of (Trivial_Algebra S) is_isomorphism A, Trivial_Algebra S
A is non-empty by A2;
hence the ManySortedFunction of the Sorts of A, the Sorts of (Trivial_Algebra S) is_epimorphism A, Trivial_Algebra S by Th25; :: according to MSUALG_3:def 10 :: thesis: the ManySortedFunction of the Sorts of A, the Sorts of (Trivial_Algebra S) is_monomorphism A, Trivial_Algebra S
hence the ManySortedFunction of the Sorts of A, the Sorts of (Trivial_Algebra S) is_homomorphism A, Trivial_Algebra S ; :: according to MSUALG_3:def 9 :: thesis: the ManySortedFunction of the Sorts of A, the Sorts of (Trivial_Algebra S) is "1-1"
F1 is "1-1" by Th10;
hence the ManySortedFunction of the Sorts of A, the Sorts of (Trivial_Algebra S) is "1-1" ; :: thesis: verum