let S be non empty non void ManySortedSign ; for V being V2() ManySortedSet of the carrier of S
for A being MSAlgebra over S
for s being SortSymbol of S
for v being Element of V . s holds root-tree [v,s] is c-Term of A,V
let V be V2() ManySortedSet of the carrier of S; for A being MSAlgebra over S
for s being SortSymbol of S
for v being Element of V . s holds root-tree [v,s] is c-Term of A,V
let A be MSAlgebra over S; for s being SortSymbol of S
for v being Element of V . s holds root-tree [v,s] is c-Term of A,V
let s be SortSymbol of S; for v being Element of V . s holds root-tree [v,s] is c-Term of A,V
let v be Element of V . s; root-tree [v,s] is c-Term of A,V
( the Sorts of A (\/) V) . s = ( the Sorts of A . s) \/ (V . s)
by PBOOLE:def 4;
then
v in ( the Sorts of A (\/) V) . s
by XBOOLE_0:def 3;
then reconsider vs = [v,s] as Terminal of (DTConMSA ( the Sorts of A (\/) V)) by MSAFREE:7;
root-tree vs in TS (DTConMSA ( the Sorts of A (\/) V))
;
hence
root-tree [v,s] is c-Term of A,V
; verum