let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra of 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 of 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;
consider F being ManySortedFunction of the Sorts of A, the Sorts of (Trivial_Algebra S);
reconsider F1 = F as ManySortedFunction of {X}, the Sorts of (Trivial_Algebra S) by A2;
take F ; :: according to MSUALG_3:def 13 :: thesis: F is_isomorphism A, Trivial_Algebra S
A is non-empty by A2, MSUALG_1:def 8;
hence F is_epimorphism A, Trivial_Algebra S by Th26; :: according to MSUALG_3:def 12 :: thesis: F is_monomorphism A, Trivial_Algebra S
hence F is_homomorphism A, Trivial_Algebra S by MSUALG_3:def 10; :: according to MSUALG_3:def 11 :: thesis: F is "1-1"
F1 is "1-1" by Th11;
hence F is "1-1" ; :: thesis: verum