let f, g be Function; :: thesis: ( dom f = X & ( for x being object st x in X holds

f . x = Im (W,x) ) & dom g = X & ( for x being object st x in X holds

g . x = Im (W,x) ) implies f = g )

assume that

A1: dom f = X and

A2: for x being object st x in X holds

f . x = Im (W,x) and

A3: dom g = X and

A4: for x being object st x in X holds

g . x = Im (W,x) ; :: thesis: f = g

f . x = Im (W,x) ) & dom g = X & ( for x being object st x in X holds

g . x = Im (W,x) ) implies f = g )

assume that

A1: dom f = X and

A2: for x being object st x in X holds

f . x = Im (W,x) and

A3: dom g = X and

A4: for x being object st x in X holds

g . x = Im (W,x) ; :: thesis: f = g

now :: thesis: for x being object st x in X holds

f . x = g . x

hence
f = g
by A1, A3, FUNCT_1:2; :: thesis: verumf . x = g . x

let x be object ; :: thesis: ( x in X implies f . x = g . x )

assume A5: x in X ; :: thesis: f . x = g . x

hence f . x = Im (W,x) by A2

.= g . x by A4, A5 ;

:: thesis: verum

end;assume A5: x in X ; :: thesis: f . x = g . x

hence f . x = Im (W,x) by A2

.= g . x by A4, A5 ;

:: thesis: verum