let S be non empty non void ManySortedSign ; for U0 being free feasible MSAlgebra of S
for A being free GeneratorSet of U0
for Z being MSSubset of U0 st Z c= A & GenMSAlg Z is feasible holds
GenMSAlg Z is free
let U0 be free feasible MSAlgebra of S; for A being free GeneratorSet of U0
for Z being MSSubset of U0 st Z c= A & GenMSAlg Z is feasible holds
GenMSAlg Z is free
let A be free GeneratorSet of U0; for Z being MSSubset of U0 st Z c= A & GenMSAlg Z is feasible holds
GenMSAlg Z is free
let Z be MSSubset of U0; ( Z c= A & GenMSAlg Z is feasible implies GenMSAlg Z is free )
assume that
A1:
Z c= A
and
A2:
GenMSAlg Z is feasible
; GenMSAlg Z is free
reconsider Z1 = Z as MSSubset of (GenMSAlg Z) by MSUALG_2:def 18;
the Sorts of (GenMSAlg Z1) = the Sorts of (GenMSAlg Z)
by EXTENS_1:22;
then reconsider z = Z as GeneratorSet of GenMSAlg Z by MSAFREE:def 4;
reconsider z1 = z as ManySortedSubset of A by A1, PBOOLE:def 23;
take
z
; MSAFREE:def 6 z is free
z is free
proof
reconsider D = the
Sorts of
(GenMSAlg Z) as
MSSubset of
U0 by MSUALG_2:def 10;
let U1 be
non-empty MSAlgebra of
S;
MSAFREE:def 5 for b1 being ManySortedFunction of z,the Sorts of U1 ex b2 being ManySortedFunction of the Sorts of (GenMSAlg Z),the Sorts of U1 st
( b2 is_homomorphism GenMSAlg Z,U1 & b2 || z = b1 )let g be
ManySortedFunction of
z,the
Sorts of
U1;
ex b1 being ManySortedFunction of the Sorts of (GenMSAlg Z),the Sorts of U1 st
( b1 is_homomorphism GenMSAlg Z,U1 & b1 || z = g )
consider G being
ManySortedFunction of
A,the
Sorts of
U1 such that A3:
G || z1 = g
by Th7;
consider h being
ManySortedFunction of
U0,
U1 such that A4:
h is_homomorphism U0,
U1
and A5:
h || A = G
by MSAFREE:def 5;
reconsider H =
h || D as
ManySortedFunction of
(GenMSAlg Z),
U1 ;
take
H
;
( H is_homomorphism GenMSAlg Z,U1 & H || z = g )
thus
H is_homomorphism GenMSAlg Z,
U1
by A2, A4, Th24;
H || z = g
thus g =
h || Z
by A3, A5, Th6
.=
H || z
by Th6
;
verum
end;
hence
z is free
; verum