let u1, u2 be UnOp of (Class R); :: thesis: ( ( for x, y being set st x in Class R & y in x holds

u1 . x = Class (R,(u . y)) ) & ( for x, y being set st x in Class R & y in x holds

u2 . x = Class (R,(u . y)) ) implies u1 = u2 )

assume that

A15: for x, y being set st x in Class R & y in x holds

u1 . x = Class (R,(u . y)) and

A16: for x, y being set st x in Class R & y in x holds

u2 . x = Class (R,(u . y)) ; :: thesis: u1 = u2

u1 . x = Class (R,(u . y)) ) & ( for x, y being set st x in Class R & y in x holds

u2 . x = Class (R,(u . y)) ) implies u1 = u2 )

assume that

A15: for x, y being set st x in Class R & y in x holds

u1 . x = Class (R,(u . y)) and

A16: for x, y being set st x in Class R & y in x holds

u2 . x = Class (R,(u . y)) ; :: thesis: u1 = u2

now :: thesis: for x being object st x in Class R holds

u1 . x = u2 . x

hence
u1 = u2
by FUNCT_2:12; :: thesis: verumu1 . x = u2 . x

let x be object ; :: thesis: ( x in Class R implies u1 . x = u2 . x )

assume A17: x in Class R ; :: thesis: u1 . x = u2 . x

then consider y being object such that

A18: y in D and

A19: x = Class (R,y) by EQREL_1:def 3;

u1 . x = Class (R,(u . y)) by A15, A17, A18, A19, EQREL_1:20;

hence u1 . x = u2 . x by A16, A17, A18, A19, EQREL_1:20; :: thesis: verum

end;assume A17: x in Class R ; :: thesis: u1 . x = u2 . x

then consider y being object such that

A18: y in D and

A19: x = Class (R,y) by EQREL_1:def 3;

u1 . x = Class (R,(u . y)) by A15, A17, A18, A19, EQREL_1:20;

hence u1 . x = u2 . x by A16, A17, A18, A19, EQREL_1:20; :: thesis: verum