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 holds deg (x -term) = 0
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 holds deg (x -term) = 0
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for x being Element of X . s holds deg (x -term) = 0
let x be Element of X . s; :: thesis: deg (x -term) = 0
set t = x -term ;
assume deg (x -term) <> 0 ; :: thesis: contradiction
then not (x -term) " [: the carrier' of S,{ the carrier of S}:] is empty ;
then consider a being object such that
A1: a in (x -term) " [: the carrier' of S,{ the carrier of S}:] by XBOOLE_0:7;
reconsider ta = (x -term) . a as set ;
A4: ( ta in [: the carrier' of S,{ the carrier of S}:] & a in dom (x -term) ) by A1, FUNCT_1:def 7;
( ta in rng (x -term) & rng (x -term) = {[x,s]} ) by A4, FUNCT_1:def 3, FUNCOP_1:8;
then ta = [x,s] by TARSKI:def 1;
then ( s in the carrier of S & the carrier of S = s ) by A4, ZFMISC_1:106;
hence contradiction ; :: thesis: verum