let S be non empty non void ManySortedSign ; 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; ( 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}
; 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)
; MSUALG_3:def 11 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; MSUALG_3:def 10 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
; MSUALG_3:def 9 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"
; verum