let f, g be ClosureOperator of the Sorts of D; :: thesis: ( ( for x being Element of Bool the Sorts of D holds f . x = Cl x ) & ( for x being Element of Bool the Sorts of D holds g . x = Cl x ) implies f = g )
assume that
A2: for x being Element of Bool the Sorts of D holds f . x = Cl x and
A3: for x being Element of Bool the Sorts of D holds g . x = Cl x ; :: thesis: f = g

now :: thesis: ( Bool the Sorts of D = dom f & Bool the Sorts of D = dom g & ( for x being object st x in Bool the Sorts of D holds
f . x = g . x ) )

set X = Bool the Sorts of D;
thus Bool the Sorts of D = dom f by FUNCT_2:def 1; :: thesis: ( Bool the Sorts of D = dom g & ( for x being object st x in Bool the Sorts of D holds
f . x = g . x ) )
thus Bool the Sorts of D = dom g by FUNCT_2:def 1; :: thesis: for x being object st x in Bool the Sorts of D holds
f . x = g . x
let x be object ; :: thesis: ( x in Bool the Sorts of D implies f . x = g . x )
assume x in Bool the Sorts of D ; :: thesis: f . x = g . x
then reconsider x1 = x as Element of Bool the Sorts of D ;
thus f . x = Cl x1 by A2
.= g . x by A3 ; :: thesis: verum

end;

hence f = g ; :: thesis: verum