let D be non empty set ; :: thesis: for f, g being non empty quasi_total Element of HFuncs D st arity f = 0 & arity g = 0 & f . {} = g . {} holds
f = g
set X = D;
let f, g be non empty quasi_total Element of HFuncs D; :: thesis: ( arity f = 0 & arity g = 0 & f . {} = g . {} implies f = g )
assume that
A1: arity f = 0 and
A2: arity g = 0 and
A3: f . {} = g . {} ; :: thesis: f = g
now :: thesis: ( dom f = {(<*> D)} & dom g = {(<*> D)} & ( for x being object st x in {(<*> D)} holds
f . x = g . x ) )
thus dom f = 0 -tuples_on D by A1, Th21
.= {(<*> D)} by FINSEQ_2:94 ; :: thesis: ( dom g = {(<*> D)} & ( for x being object st x in {(<*> D)} holds
f . x = g . x ) )
thus dom g = 0 -tuples_on D by A2, Th21
.= {(<*> D)} by FINSEQ_2:94 ; :: thesis: for x being object st x in {(<*> D)} holds
f . x = g . x
let x be object ; :: thesis: ( x in {(<*> D)} implies f . x = g . x )
assume x in {(<*> D)} ; :: thesis: f . x = g . x
then x = {} by TARSKI:def 1;
hence f . x = g . x by A3; :: thesis: verum
end;
hence f = g ; :: thesis: verum