let S be non empty non void ManySortedSign ; :: thesis: for X being V2() ManySortedSet of the carrier of S
for A being b1,S -terms MSAlgebra over S ex VF being ManySortedMSSet of the Sorts of A, the Sorts of A ex B being b1,S -terms 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 MSAlgebra over S ex VF being ManySortedMSSet of the Sorts of A, the Sorts of A ex B being X,S -terms 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 MSAlgebra over S; :: thesis: ex VF being ManySortedMSSet of the Sorts of A, the Sorts of A ex B being X,S -terms VarMSAlgebra over S st
( B = VarMSAlgebra(# the Sorts of A, the Charact of A,VF #) & B is vf-free )
deffunc H1( 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 H1(s,r,t) is Subset of ( the Sorts of A . r)
proof
let s, r be SortSymbol of S; :: thesis: for t being Element of A,s holds H1(s,r,t) is Subset of ( the Sorts of A . r)
let t be Element of the Sorts of A . s; :: thesis: H1(s,r,t) is Subset of ( the Sorts of A . r)
H1(s,r,t) c= the Sorts of A . r
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in H1(s,r,t) or x in the Sorts of A . r )
assume x in H1(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:43;
reconsider t1 = tp as Term of S,X by MSAFREE4:41;
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;
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:42; :: thesis: verum
end;
suppose tp . {} in [: the carrier' of S,{ the carrier of S}:] ; :: thesis: x in the Sorts of A . r
then (tp . {}) `2 in { the carrier of S} by MCART_1:10;
then ( r = the carrier of S & r in the carrier of S ) by A2, TARSKI:def 1;
hence x in the Sorts of A . r ; :: thesis: verum
end;
end;
end;
hence H1(s,r,t) is Subset of ( the Sorts of A . r) ; :: thesis: verum
end;
consider v being ManySortedMSSet of the Sorts of A, the Sorts of A such that
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 = H1(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 VarMSAlgebra over S st
( B = VarMSAlgebra(# the Sorts of A, the Charact of A,v #) & B is vf-free )
A6: VarMSAlgebra(# the Sorts of A, the Charact of A,v #) is X,S -terms
proof
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: ( FreeGen X is ManySortedSubset of the Sorts of VarMSAlgebra(# the Sorts of A, the Charact of A,v #) & ( for b1 being Element of the carrier' of S
for b2 being set holds
( not b2 in Args (b1,(Free (S,X))) or not (Den (b1,(Free (S,X)))) . b2 in the Sorts of VarMSAlgebra(# the Sorts of A, the Charact of A,v #) . (the_result_sort_of b1) or ( b2 in Args (b1,VarMSAlgebra(# the Sorts of A, the Charact of A,v #)) & (Den (b1,VarMSAlgebra(# the Sorts of A, the Charact of A,v #))) . b2 = (Den (b1,(Free (S,X)))) . b2 ) ) ) & ( for b1 being ManySortedFunction of FreeGen X, the Sorts of VarMSAlgebra(# the Sorts of A, the Charact of A,v #)
for b2 being ManySortedSubset of the Sorts of VarMSAlgebra(# the Sorts of A, the Charact of A,v #) holds
( not b2 = FreeGen X or ex b3 being ManySortedFunction of the Sorts of VarMSAlgebra(# the Sorts of A, the Charact of A,v #), the Sorts of VarMSAlgebra(# the Sorts of A, the Charact of A,v #) st
( b3 is_homomorphism VarMSAlgebra(# the Sorts of A, the Charact of A,v #), VarMSAlgebra(# the Sorts of A, the Charact of A,v #) & b1 = b3 || b2 ) ) ) )
thus FreeGen X is ManySortedSubset of the Sorts of VarMSAlgebra(# the Sorts of A, the Charact of A,v #) by MSAFREE4:def 6; :: thesis: ( ( for b1 being Element of the carrier' of S
for b2 being set holds
( not b2 in Args (b1,(Free (S,X))) or not (Den (b1,(Free (S,X)))) . b2 in the Sorts of VarMSAlgebra(# the Sorts of A, the Charact of A,v #) . (the_result_sort_of b1) or ( b2 in Args (b1,VarMSAlgebra(# the Sorts of A, the Charact of A,v #)) & (Den (b1,VarMSAlgebra(# the Sorts of A, the Charact of A,v #))) . b2 = (Den (b1,(Free (S,X)))) . b2 ) ) ) & ( for b1 being ManySortedFunction of FreeGen X, the Sorts of VarMSAlgebra(# the Sorts of A, the Charact of A,v #)
for b2 being ManySortedSubset of the Sorts of VarMSAlgebra(# the Sorts of A, the Charact of A,v #) holds
( not b2 = FreeGen X or ex b3 being ManySortedFunction of the Sorts of VarMSAlgebra(# the Sorts of A, the Charact of A,v #), the Sorts of VarMSAlgebra(# the Sorts of A, the Charact of A,v #) st
( b3 is_homomorphism VarMSAlgebra(# the Sorts of A, the Charact of A,v #), VarMSAlgebra(# the Sorts of A, the Charact of A,v #) & b1 = b3 || b2 ) ) ) )
hereby :: thesis: for b1 being ManySortedFunction of FreeGen X, the Sorts of VarMSAlgebra(# the Sorts of A, the Charact of A,v #)
for b2 being ManySortedSubset of the Sorts of VarMSAlgebra(# the Sorts of A, the Charact of A,v #) holds
( not b2 = FreeGen X or ex b3 being ManySortedFunction of the Sorts of VarMSAlgebra(# the Sorts of A, the Charact of A,v #), the Sorts of VarMSAlgebra(# the Sorts of A, the Charact of A,v #) st
( b3 is_homomorphism VarMSAlgebra(# the Sorts of A, the Charact of A,v #), VarMSAlgebra(# the Sorts of A, the Charact of A,v #) & b1 = b3 || b2 ) )
let 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 VarMSAlgebra(# the Sorts of A, the Charact of A,v #) . (the_result_sort_of o) holds
( p in Args (o,VarMSAlgebra(# the Sorts of A, the Charact of A,v #)) & (Den (o,VarMSAlgebra(# the Sorts of A, the Charact of A,v #))) . 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 VarMSAlgebra(# the Sorts of A, the Charact of A,v #) . (the_result_sort_of o) implies ( p in Args (o,VarMSAlgebra(# the Sorts of A, the Charact of A,v #)) & (Den (o,VarMSAlgebra(# the Sorts of A, the Charact of A,v #))) . 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 VarMSAlgebra(# the Sorts of A, the Charact of A,v #) . (the_result_sort_of o) ) ; :: thesis: ( p in Args (o,VarMSAlgebra(# the Sorts of A, the Charact of A,v #)) & (Den (o,VarMSAlgebra(# the Sorts of A, the Charact of A,v #))) . 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 6;
hence ( p in Args (o,VarMSAlgebra(# the Sorts of A, the Charact of A,v #)) & (Den (o,VarMSAlgebra(# the Sorts of A, the Charact of A,v #))) . p = (Den (o,(Free (S,X)))) . p ) ; :: thesis: verum
end;
let f be ManySortedFunction of FreeGen X, the Sorts of VarMSAlgebra(# the Sorts of A, the Charact of A,v #); :: thesis: for b1 being ManySortedSubset of the Sorts of VarMSAlgebra(# the Sorts of A, the Charact of A,v #) holds
( not b1 = FreeGen X or ex b2 being ManySortedFunction of the Sorts of VarMSAlgebra(# the Sorts of A, the Charact of A,v #), the Sorts of VarMSAlgebra(# the Sorts of A, the Charact of A,v #) st
( b2 is_homomorphism VarMSAlgebra(# the Sorts of A, the Charact of A,v #), VarMSAlgebra(# the Sorts of A, the Charact of A,v #) & f = b2 || b1 ) )
let G be ManySortedSubset of the Sorts of VarMSAlgebra(# the Sorts of A, the Charact of A,v #); :: thesis: ( not G = FreeGen X or ex b1 being ManySortedFunction of the Sorts of VarMSAlgebra(# the Sorts of A, the Charact of A,v #), the Sorts of VarMSAlgebra(# the Sorts of A, the Charact of A,v #) st
( b1 is_homomorphism VarMSAlgebra(# the Sorts of A, the Charact of A,v #), VarMSAlgebra(# the Sorts of A, the Charact of A,v #) & f = b1 || G ) )
assume A7: G = FreeGen X ; :: thesis: ex b1 being ManySortedFunction of the Sorts of VarMSAlgebra(# the Sorts of A, the Charact of A,v #), the Sorts of VarMSAlgebra(# the Sorts of A, the Charact of A,v #) st
( b1 is_homomorphism VarMSAlgebra(# the Sorts of A, the Charact of A,v #), VarMSAlgebra(# the Sorts of A, the Charact of A,v #) & f = b1 || 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 6;
reconsider g = h as ManySortedFunction of VarMSAlgebra(# the Sorts of A, the Charact of A,v #),VarMSAlgebra(# the Sorts of A, the Charact of A,v #) ;
take g ; :: thesis: ( g is_homomorphism VarMSAlgebra(# the Sorts of A, the Charact of A,v #), VarMSAlgebra(# the Sorts of A, the Charact of A,v #) & f = g || G )
MSAlgebra(# the Sorts of VarMSAlgebra(# the Sorts of A, the Charact of A,v #), the Charact of VarMSAlgebra(# the Sorts of A, the Charact of A,v #) #) = MSAlgebra(# the Sorts of A, the Charact of A #) ;
hence g is_homomorphism VarMSAlgebra(# the Sorts of A, the Charact of A,v #), VarMSAlgebra(# the Sorts of A, the Charact of A,v #) by A8, MSAFREE4:30; :: thesis: f = g || G
thus f = g || G by A8; :: thesis: verum
end;
reconsider B = VarMSAlgebra(# the Sorts of A, the Charact of A,v #) as X,S -terms strict VarMSAlgebra over S by A6;
B is vf-free by A5;
hence ex B being X,S -terms VarMSAlgebra over S st
( B = VarMSAlgebra(# the Sorts of A, the Charact of A,v #) & B is vf-free ) ; :: thesis: verum