let S be non empty non void ManySortedSign ; :: thesis: for s being SortSymbol of S
for X being non-empty ManySortedSet of the carrier of S
for x being Element of X . s
for T being b₂,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for r being Element of T st x nin vf r holds
r is x -omitting
let s be SortSymbol of S; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for x being Element of X . s
for T being b₁,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for r being Element of T st x nin vf r holds
r is x -omitting
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for x being Element of X . s
for T being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for r being Element of T st x nin vf r holds
r is x -omitting
let x be Element of X . s; :: thesis: for T being X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for r being Element of T st x nin vf r holds
r is x -omitting
let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis: for r being Element of T st x nin vf r holds
r is x -omitting
let r be Element of T; :: thesis: ( x nin vf r implies r is x -omitting )
assume x nin vf r ; :: thesis: r is x -omitting
then A1: [x,s] nin (rng r) /\ [:(Union X), the carrier of S:] by XTUPLE_0:def 12;
[x,s] in [:(Union X), the carrier of S:] by ZFMISC_1:87;
then [x,s] nin rng r by A1, XBOOLE_0:def 4;
hence Coim (r,[x,s]) = {} by FUNCT_1:72; :: according to MSAFREE5:def 21 :: thesis: verum