let S be non empty non void ManySortedSign ; :: thesis: for X being V2() ManySortedSet of the carrier of S

for A being b_{1},S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S ex VF being ManySortedMSSet of the Sorts of A, the Sorts of A ex B being b_{1},S -terms all_vars_including inheriting_operations free_in_itself VarMSAlgebra over S st

( B = VarMSAlgebra(# the Sorts of A, the Charact of A,VF #) & B is vf-free )

let X be V2() ManySortedSet of the carrier of S; :: thesis: for A being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S ex VF being ManySortedMSSet of the Sorts of A, the Sorts of A ex B being X,S -terms all_vars_including inheriting_operations free_in_itself VarMSAlgebra over S st

( B = VarMSAlgebra(# the Sorts of A, the Charact of A,VF #) & B is vf-free )

let A be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis: ex VF being ManySortedMSSet of the Sorts of A, the Sorts of A ex B being X,S -terms all_vars_including inheriting_operations free_in_itself VarMSAlgebra over S st

( B = VarMSAlgebra(# the Sorts of A, the Charact of A,VF #) & B is vf-free )

deffunc H_{1}( Element of S, Element of S, Element of A,$1) -> set = { ($3 | p) where p is Element of dom $3 : (($3 | p) . {}) `2 = $2 } ;

A1: for s, r being SortSymbol of S

for t being Element of A,s holds H_{1}(s,r,t) is Subset of ( the Sorts of A . r)

A5: for x, z being Element of the carrier of S

for y being Element of the Sorts of A . x holds ((v . x) . y) . z = H_{1}(x,z,y)
from AOFA_A00:sch 1(A1);

set B = VarMSAlgebra(# the Sorts of A, the Charact of A,v #);

take v ; :: thesis: ex B being X,S -terms all_vars_including inheriting_operations free_in_itself VarMSAlgebra over S st

( B = VarMSAlgebra(# the Sorts of A, the Charact of A,v #) & B is vf-free )

VarMSAlgebra(# the Sorts of A, the Charact of A,v #) is X,S -terms

( B is all_vars_including & B is inheriting_operations & B is free_in_itself )

B is vf-free by A5;

hence ex B being X,S -terms all_vars_including inheriting_operations free_in_itself VarMSAlgebra over S st

( B = VarMSAlgebra(# the Sorts of A, the Charact of A,v #) & B is vf-free ) ; :: thesis: verum

for A being b

( B = VarMSAlgebra(# the Sorts of A, the Charact of A,VF #) & B is vf-free )

let X be V2() ManySortedSet of the carrier of S; :: thesis: for A being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S ex VF being ManySortedMSSet of the Sorts of A, the Sorts of A ex B being X,S -terms all_vars_including inheriting_operations free_in_itself VarMSAlgebra over S st

( B = VarMSAlgebra(# the Sorts of A, the Charact of A,VF #) & B is vf-free )

let A be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis: ex VF being ManySortedMSSet of the Sorts of A, the Sorts of A ex B being X,S -terms all_vars_including inheriting_operations free_in_itself VarMSAlgebra over S st

( B = VarMSAlgebra(# the Sorts of A, the Charact of A,VF #) & B is vf-free )

deffunc H

A1: for s, r being SortSymbol of S

for t being Element of A,s holds H

proof

consider v being ManySortedMSSet of the Sorts of A, the Sorts of A such that
let s, r be SortSymbol of S; :: thesis: for t being Element of A,s holds H_{1}(s,r,t) is Subset of ( the Sorts of A . r)

let t be Element of the Sorts of A . s; :: thesis: H_{1}(s,r,t) is Subset of ( the Sorts of A . r)

H_{1}(s,r,t) c= the Sorts of A . r
_{1}(s,r,t) is Subset of ( the Sorts of A . r)
; :: thesis: verum

end;let t be Element of the Sorts of A . s; :: thesis: H

H

proof

hence
H
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H_{1}(s,r,t) or x in the Sorts of A . r )

assume x in H_{1}(s,r,t)
; :: thesis: x in the Sorts of A . r

then consider p being Element of dom t such that

A2: ( x = t | p & ((t | p) . {}) `2 = r ) ;

reconsider tp = t | p as Element of A by MSAFREE4:44;

reconsider t1 = tp as Term of S,X by MSAFREE4:42;

end;assume x in H

then consider p being Element of dom t such that

A2: ( x = t | p & ((t | p) . {}) `2 = r ) ;

reconsider tp = t | p as Element of A by MSAFREE4:44;

reconsider t1 = tp as Term of S,X by MSAFREE4:42;

per cases
( ex s being SortSymbol of S ex v being Element of X . s st t1 . {} = [v,s] or tp . {} in [: the carrier' of S,{ the carrier of S}:] )
by MSATERM:2;

end;

suppose
ex s being SortSymbol of S ex v being Element of X . s st t1 . {} = [v,s]
; :: thesis: x in the Sorts of A . r

then consider s1 being SortSymbol of S, v being Element of X . s1 such that

A3: tp . {} = [v,s1] ;

A4: s1 = r by A2, A3;

then t1 = root-tree [v,r] by A3, MSATERM:5;

then the_sort_of t1 = r by A4, MSATERM:14;

then t1 in FreeSort (X,r) by MSATERM:def 5;

then tp in the Sorts of (FreeMSA X) . r by MSAFREE:def 11;

then tp in the Sorts of (Free (S,X)) . r by MSAFREE3:31;

hence x in the Sorts of A . r by A2, MSAFREE4:43; :: thesis: verum

end;A3: tp . {} = [v,s1] ;

A4: s1 = r by A2, A3;

then t1 = root-tree [v,r] by A3, MSATERM:5;

then the_sort_of t1 = r by A4, MSATERM:14;

then t1 in FreeSort (X,r) by MSATERM:def 5;

then tp in the Sorts of (FreeMSA X) . r by MSAFREE:def 11;

then tp in the Sorts of (Free (S,X)) . r by MSAFREE3:31;

hence x in the Sorts of A . r by A2, MSAFREE4:43; :: thesis: verum

A5: for x, z being Element of the carrier of S

for y being Element of the Sorts of A . x holds ((v . x) . y) . z = H

set B = VarMSAlgebra(# the Sorts of A, the Charact of A,v #);

take v ; :: thesis: ex B being X,S -terms all_vars_including inheriting_operations free_in_itself VarMSAlgebra over S st

( B = VarMSAlgebra(# the Sorts of A, the Charact of A,v #) & B is vf-free )

VarMSAlgebra(# the Sorts of A, the Charact of A,v #) is X,S -terms

proof

then reconsider B = VarMSAlgebra(# the Sorts of A, the Charact of A,v #) as X,S -terms strict VarMSAlgebra over S ;
thus
the Sorts of VarMSAlgebra(# the Sorts of A, the Charact of A,v #) is ManySortedSubset of the Sorts of (Free (S,X))
by MSAFREE4:def 6; :: according to MSAFREE4:def 6 :: thesis: verum

end;( B is all_vars_including & B is inheriting_operations & B is free_in_itself )

proof

then reconsider B = B as X,S -terms all_vars_including inheriting_operations free_in_itself strict VarMSAlgebra over S ;
thus
FreeGen X is ManySortedSubset of the Sorts of B
by MSAFREE4:def 7; :: according to MSAFREE4:def 7 :: thesis: ( B is inheriting_operations & B is free_in_itself )

_{1} being ManySortedSubset of the Sorts of B holds

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

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

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

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

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

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

reconsider H = G as MSSubset of A ;

consider h being ManySortedFunction of A,A such that

A8: ( h is_homomorphism A,A & f = h || H ) by A7, MSAFREE4:def 9;

reconsider g = h as ManySortedFunction of B,B ;

take g ; :: thesis: ( g is_homomorphism B,B & f = g || G )

MSAlgebra(# the Sorts of B, the Charact of B #) = MSAlgebra(# the Sorts of A, the Charact of A #) ;

hence g is_homomorphism B,B by A8, MSAFREE4:30; :: thesis: f = g || G

thus f = g || G by A8; :: thesis: verum

end;hereby :: according to MSAFREE4:def 8 :: thesis: B is free_in_itself

let f be ManySortedFunction of FreeGen X, the Sorts of B; :: according to MSAFREE4:def 9 :: thesis: for blet o be OperSymbol of S; :: thesis: for p being FinSequence st p in Args (o,(Free (S,X))) & (Den (o,(Free (S,X)))) . p in the Sorts of B . (the_result_sort_of o) holds

( p in Args (o,B) & (Den (o,B)) . p = (Den (o,(Free (S,X)))) . p )

let p be FinSequence; :: thesis: ( p in Args (o,(Free (S,X))) & (Den (o,(Free (S,X)))) . p in the Sorts of B . (the_result_sort_of o) implies ( p in Args (o,B) & (Den (o,B)) . p = (Den (o,(Free (S,X)))) . p ) )

assume ( p in Args (o,(Free (S,X))) & (Den (o,(Free (S,X)))) . p in the Sorts of B . (the_result_sort_of o) ) ; :: thesis: ( p in Args (o,B) & (Den (o,B)) . p = (Den (o,(Free (S,X)))) . p )

then ( p in Args (o,A) & (Den (o,A)) . p = (Den (o,(Free (S,X)))) . p ) by MSAFREE4:def 8;

hence ( p in Args (o,B) & (Den (o,B)) . p = (Den (o,(Free (S,X)))) . p ) ; :: thesis: verum

end;( p in Args (o,B) & (Den (o,B)) . p = (Den (o,(Free (S,X)))) . p )

let p be FinSequence; :: thesis: ( p in Args (o,(Free (S,X))) & (Den (o,(Free (S,X)))) . p in the Sorts of B . (the_result_sort_of o) implies ( p in Args (o,B) & (Den (o,B)) . p = (Den (o,(Free (S,X)))) . p ) )

assume ( p in Args (o,(Free (S,X))) & (Den (o,(Free (S,X)))) . p in the Sorts of B . (the_result_sort_of o) ) ; :: thesis: ( p in Args (o,B) & (Den (o,B)) . p = (Den (o,(Free (S,X)))) . p )

then ( p in Args (o,A) & (Den (o,A)) . p = (Den (o,(Free (S,X)))) . p ) by MSAFREE4:def 8;

hence ( p in Args (o,B) & (Den (o,B)) . p = (Den (o,(Free (S,X)))) . p ) ; :: thesis: verum

( not b

( b

let G be ManySortedSubset of the Sorts of B; :: thesis: ( not G = FreeGen X or ex b

( b

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

( b

reconsider H = G as MSSubset of A ;

consider h being ManySortedFunction of A,A such that

A8: ( h is_homomorphism A,A & f = h || H ) by A7, MSAFREE4:def 9;

reconsider g = h as ManySortedFunction of B,B ;

take g ; :: thesis: ( g is_homomorphism B,B & f = g || G )

MSAlgebra(# the Sorts of B, the Charact of B #) = MSAlgebra(# the Sorts of A, the Charact of A #) ;

hence g is_homomorphism B,B by A8, MSAFREE4:30; :: thesis: f = g || G

thus f = g || G by A8; :: thesis: verum

B is vf-free by A5;

hence ex B being X,S -terms all_vars_including inheriting_operations free_in_itself VarMSAlgebra over S st

( B = VarMSAlgebra(# the Sorts of A, the Charact of A,v #) & B is vf-free ) ; :: thesis: verum