let i be Nat; :: thesis: for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of the carrier of S
for T being b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for r being Element of T holds
( r in T deg<= i iff deg r <= i )
let S be non empty non void ManySortedSign ; :: thesis: for X being V5() ManySortedSet of the carrier of S
for T being b₁,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S
for r being Element of T holds
( r in T deg<= i iff deg r <= i )
let X be V5() ManySortedSet of the carrier of 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 holds
( r in T deg<= i iff deg r <= i )
let T be X,S -terms all_vars_including inheriting_operations free_in_itself MSAlgebra over S; :: thesis: for r being Element of T holds
( r in T deg<= i iff deg r <= i )
let r be Element of T; :: thesis: ( r in T deg<= i iff deg r <= i )
( r in T deg<= i iff ex r1 being Element of T st
( r = r1 & deg r1 <= i ) ) ;
hence ( r in T deg<= i iff deg r <= i ) ; :: thesis: verum