set v = the ManySortedMSSet of the Sorts of (Free (S,X)), the Sorts of (Free (S,X));

set A = VarMSAlgebra(# the Sorts of (Free (S,X)), the Charact of (Free (S,X)), the ManySortedMSSet of the Sorts of (Free (S,X)), the Sorts of (Free (S,X)) #);

VarMSAlgebra(# the Sorts of (Free (S,X)), the Charact of (Free (S,X)), the ManySortedMSSet of the Sorts of (Free (S,X)), the Sorts of (Free (S,X)) #) is X,S -terms

take A ; :: thesis: ( A is all_vars_including & A is inheriting_operations & A is free_in_itself )

A1: MSAlgebra(# the Sorts of A, the Charact of A #) = FreeMSA X by MSAFREE3:31;

thus ( FreeGen X is ManySortedSubset of the Sorts of A & ( for o being OperSymbol of S

for p being FinSequence st p in Args (o,(Free (S,X))) & (Den (o,(Free (S,X)))) . p in the Sorts of A . (the_result_sort_of o) holds

( p in Args (o,A) & (Den (o,A)) . p = (Den (o,(Free (S,X)))) . p ) ) ) by MSAFREE3:31; :: according to MSAFREE4:def 7,MSAFREE4:def 8 :: thesis: A is free_in_itself

reconsider B = A as non-empty VarMSAlgebra over S ;

let f be ManySortedFunction of FreeGen X, the Sorts of A; :: according to MSAFREE4:def 9 :: thesis: for b_{1} being ManySortedSubset of the Sorts of A holds

( not b_{1} = FreeGen X or ex b_{2} being ManySortedFunction of the Sorts of A, the Sorts of A st

( b_{2} is_homomorphism A,A & f = b_{2} || b_{1} ) )

let G be MSSubset of A; :: thesis: ( not G = FreeGen X or ex b_{1} being ManySortedFunction of the Sorts of A, the Sorts of A st

( b_{1} is_homomorphism A,A & f = b_{1} || G ) )

assume A2: G = FreeGen X ; :: thesis: ex b_{1} being ManySortedFunction of the Sorts of A, the Sorts of A st

( b_{1} is_homomorphism A,A & f = b_{1} || G )

then reconsider F = G as V2() GeneratorSet of MSAlgebra(# the Sorts of B, the Charact of B #) by MSAFREE3:31;

reconsider H = F as V2() GeneratorSet of B by Th32;

H is free by Th33, A1, A2, MSAFREE:16;

hence ex b_{1} being ManySortedFunction of the Sorts of A, the Sorts of A st

( b_{1} is_homomorphism A,A & f = b_{1} || G )
by A2; :: thesis: verum

set A = VarMSAlgebra(# the Sorts of (Free (S,X)), the Charact of (Free (S,X)), the ManySortedMSSet of the Sorts of (Free (S,X)), the Sorts of (Free (S,X)) #);

VarMSAlgebra(# the Sorts of (Free (S,X)), the Charact of (Free (S,X)), the ManySortedMSSet of the Sorts of (Free (S,X)), the Sorts of (Free (S,X)) #) is X,S -terms

proof

then reconsider A = VarMSAlgebra(# the Sorts of (Free (S,X)), the Charact of (Free (S,X)), the ManySortedMSSet of the Sorts of (Free (S,X)), the Sorts of (Free (S,X)) #) as X,S -terms strict VarMSAlgebra over S ;
thus
the Sorts of VarMSAlgebra(# the Sorts of (Free (S,X)), the Charact of (Free (S,X)), the ManySortedMSSet of the Sorts of (Free (S,X)), the Sorts of (Free (S,X)) #) c= the Sorts of (Free (S,X))
; :: according to PBOOLE:def 18,MSAFREE4:def 6 :: thesis: verum

end;take A ; :: thesis: ( A is all_vars_including & A is inheriting_operations & A is free_in_itself )

A1: MSAlgebra(# the Sorts of A, the Charact of A #) = FreeMSA X by MSAFREE3:31;

thus ( FreeGen X is ManySortedSubset of the Sorts of A & ( for o being OperSymbol of S

for p being FinSequence st p in Args (o,(Free (S,X))) & (Den (o,(Free (S,X)))) . p in the Sorts of A . (the_result_sort_of o) holds

( p in Args (o,A) & (Den (o,A)) . p = (Den (o,(Free (S,X)))) . p ) ) ) by MSAFREE3:31; :: according to MSAFREE4:def 7,MSAFREE4:def 8 :: thesis: A is free_in_itself

reconsider B = A as non-empty VarMSAlgebra over S ;

let f be ManySortedFunction of FreeGen X, the Sorts of A; :: according to MSAFREE4:def 9 :: thesis: for b

( not b

( b

let G be MSSubset of A; :: thesis: ( not G = FreeGen X or ex b

( b

assume A2: G = FreeGen X ; :: thesis: ex b

( b

then reconsider F = G as V2() GeneratorSet of MSAlgebra(# the Sorts of B, the Charact of B #) by MSAFREE3:31;

reconsider H = F as V2() GeneratorSet of B by Th32;

H is free by Th33, A1, A2, MSAFREE:16;

hence ex b

( b