set x = the set ;
reconsider A = { the set } as non empty set ;
set a = the Element of A;
reconsider w = (<*> A) .--> the Element of A as Element of PFuncs ((A *),A) by MARGREL1:19;
reconsider ww = <*w*> as PFuncFinSequence of A ;
set U0 = UAStr(# A,ww #);
A1:
( the charact of UAStr(# A,ww #) is quasi_total & the charact of UAStr(# A,ww #) is homogeneous )
by MARGREL1:20;
A2:
the charact of UAStr(# A,ww #) is non-empty
by MARGREL1:20;
A3:
len the charact of UAStr(# A,ww #) = 1
by FINSEQ_1:39;
reconsider U0 = UAStr(# A,ww #) as Universal_Algebra by A1, A2, UNIALG_1:def 1, UNIALG_1:def 2, UNIALG_1:def 3;
A4:
dom the charact of U0 = {1}
by A3, FINSEQ_1:2, FINSEQ_1:def 3;
1 in {1}
by TARSKI:def 1;
then reconsider o0 = the charact of U0 . 1 as operation of U0 by A4, FUNCT_1:def 3;
take
U0
; ( U0 is free & U0 is strict )
A5:
GenUnivAlg ({} the carrier of U0) = U0
A9:
o0 = w
by FINSEQ_1:40;
then A10:
dom o0 = {(<*> A)}
by FUNCOP_1:13;
then A11:
arity o0 = 0
by MARGREL1:def 25;
A12:
{} in {(<*> A)}
by TARSKI:def 1;
then
o0 . (<*> A) = the Element of A
by A9, FUNCOP_1:7;
then
the Element of A in rng o0
by A10, A12, FUNCT_1:def 3;
then
the Element of A in Constants U0
by A11;
then reconsider G = {} the carrier of U0 as GeneratorSet of U0 by A5, Lm3;
now ex G being GeneratorSet of U0 st G is free take G =
G;
G is free now for U1 being Universal_Algebra st U0,U1 are_similar holds
for f being Function of G, the carrier of U1 ex h being Function of U0,U1 st
( h is_homomorphism & h | G = f )let U1 be
Universal_Algebra;
( U0,U1 are_similar implies for f being Function of G, the carrier of U1 ex h being Function of U0,U1 st
( h is_homomorphism & h | G = f ) )A13:
1
in {1}
by TARSKI:def 1;
assume A14:
U0,
U1 are_similar
;
for f being Function of G, the carrier of U1 ex h being Function of U0,U1 st
( h is_homomorphism & h | G = f )then A15:
signature U0 = signature U1
;
len the
charact of
U1 = 1
by A3, A14, UNIALG_2:1;
then
dom the
charact of
U1 = {1}
by FINSEQ_1:2, FINSEQ_1:def 3;
then reconsider o1 = the
charact of
U1 . 1 as
operation of
U1 by A13, FUNCT_1:def 3;
A16:
rng o1 c= the
carrier of
U1
by RELAT_1:def 19;
let f be
Function of
G, the
carrier of
U1;
ex h being Function of U0,U1 st
( h is_homomorphism & h | G = f )consider aa being
object such that A17:
aa in dom o1
by XBOOLE_0:def 1;
o1 . aa in rng o1
by A17, FUNCT_1:def 3;
then reconsider u1 =
o1 . aa as
Element of
U1 by A16;
reconsider h = the
carrier of
U0 --> u1 as
Function of
U0,
U1 ;
take h =
h;
( h is_homomorphism & h | G = f )A18:
(
len (signature U0) = len the
charact of
U0 &
dom (signature U0) = Seg (len (signature U0)) )
by FINSEQ_1:def 3, UNIALG_1:def 4;
then
(signature U0) . 1
= arity o0
by A3, A13, FINSEQ_1:2, UNIALG_1:def 4;
then A19:
arity o0 = arity o1
by A3, A13, A15, A18, FINSEQ_1:2, UNIALG_1:def 4;
now for n being Nat st n in dom the charact of U0 holds
for 0o being operation of U0
for 1o being operation of U1 st 0o = the charact of U0 . n & 1o = the charact of U1 . n holds
for y being FinSequence of U0 st y in dom 0o holds
h . (0o . y) = 1o . (h * y)let n be
Nat;
( n in dom the charact of U0 implies for 0o being operation of U0
for 1o being operation of U1 st 0o = the charact of U0 . n & 1o = the charact of U1 . n holds
for y being FinSequence of U0 st y in dom 0o holds
h . (0o . y) = 1o . (h * y) )assume
n in dom the
charact of
U0
;
for 0o being operation of U0
for 1o being operation of U1 st 0o = the charact of U0 . n & 1o = the charact of U1 . n holds
for y being FinSequence of U0 st y in dom 0o holds
h . (0o . y) = 1o . (h * y)then A20:
n = 1
by A4, TARSKI:def 1;
let 0o be
operation of
U0;
for 1o being operation of U1 st 0o = the charact of U0 . n & 1o = the charact of U1 . n holds
for y being FinSequence of U0 st y in dom 0o holds
h . (0o . y) = 1o . (h * y)let 1o be
operation of
U1;
( 0o = the charact of U0 . n & 1o = the charact of U1 . n implies for y being FinSequence of U0 st y in dom 0o holds
h . (0o . y) = 1o . (h * y) )assume that A21:
0o = the
charact of
U0 . n
and A22:
1o = the
charact of
U1 . n
;
for y being FinSequence of U0 st y in dom 0o holds
h . (0o . y) = 1o . (h * y)let y be
FinSequence of
U0;
( y in dom 0o implies h . (0o . y) = 1o . (h * y) )assume A23:
y in dom 0o
;
h . (0o . y) = 1o . (h * y)then
y = <*> the
carrier of
U0
by A10, A20, A21, TARSKI:def 1;
then A24:
h * y = <*> the
carrier of
U1
;
dom 1o =
0 -tuples_on the
carrier of
U1
by A11, A19, A20, A22, MARGREL1:22
.=
{(<*> the carrier of U1)}
by FINSEQ_2:94
;
then A25:
1o . (h * y) = u1
by A17, A20, A22, A24, TARSKI:def 1;
A26:
rng 0o c= the
carrier of
U0
by RELAT_1:def 19;
0o . y in rng 0o
by A23, FUNCT_1:def 3;
hence
h . (0o . y) = 1o . (h * y)
by A25, A26, FUNCOP_1:7;
verum end; hence
h is_homomorphism
by A14, ALG_1:def 1;
h | G = f
f = {}
;
hence
h | G = f
;
verum end; hence
G is
free
;
verum end;
hence
( U0 is free & U0 is strict )
; verum