let X be ARS ; :: thesis: for x, y being Element of X st X is WN & X is UN* & x <=*=> y holds

nf x = nf y

let x, y be Element of X; :: thesis: ( X is WN & X is UN* & x <=*=> y implies nf x = nf y )

assume A1: ( X is WN & X is UN* ) ; :: thesis: ( not x <=*=> y or nf x = nf y )

assume A2: x <=*=> y ; :: thesis: nf x = nf y

defpred S_{1}[ Element of X] means nf x = nf $1;

A3: S_{1}[x]
;

A4: for z, u being Element of X st z <==> u & S_{1}[z] holds

S_{1}[u]
by A1, Th2, Lem26;

S_{1}[y]
from ABSRED_0:sch 6(A2, A3, A4);

hence nf x = nf y ; :: thesis: verum

nf x = nf y

let x, y be Element of X; :: thesis: ( X is WN & X is UN* & x <=*=> y implies nf x = nf y )

assume A1: ( X is WN & X is UN* ) ; :: thesis: ( not x <=*=> y or nf x = nf y )

assume A2: x <=*=> y ; :: thesis: nf x = nf y

defpred S

A3: S

A4: for z, u being Element of X st z <==> u & S

S

S

hence nf x = nf y ; :: thesis: verum