let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for T being b₁,S -terms all_vars_including inheriting_operations MSAlgebra over S
for G being basic GeneratorSet of T
for s being SortSymbol of S
for a being set holds
( a is pure Element of G . s iff a in (FreeGen T) . s )
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for T being X,S -terms all_vars_including inheriting_operations MSAlgebra over S
for G being basic GeneratorSet of T
for s being SortSymbol of S
for a being set holds
( a is pure Element of G . s iff a in (FreeGen T) . s )
let T be X,S -terms all_vars_including inheriting_operations MSAlgebra over S; :: thesis: for G being basic GeneratorSet of T
for s being SortSymbol of S
for a being set holds
( a is pure Element of G . s iff a in (FreeGen T) . s )
let G be basic GeneratorSet of T; :: thesis: for s being SortSymbol of S
for a being set holds
( a is pure Element of G . s iff a in (FreeGen T) . s )
let s be SortSymbol of S; :: thesis: for a being set holds
( a is pure Element of G . s iff a in (FreeGen T) . s )
let a be set ; :: thesis: ( a is pure Element of G . s iff a in (FreeGen T) . s )
(FreeGen T) . s c= G . s by Def3, PBOOLE:def 2;
hence ( a is pure Element of G . s iff a in (FreeGen T) . s ) by Def4; :: thesis: verum