let o1, o2 be UnOp of F₂(); :: thesis: ( ( for f being set st f in F₂() holds
o1 . f = F₃(f) ) & ( for f being set st f in F₂() holds
o2 . f = F₃(f) ) implies o1 = o2 )
assume that
A1: for f being set st f in F₂() holds
o1 . f = F₃(f) and
A2: for f being set st f in F₂() holds
o2 . f = F₃(f) ; :: thesis: o1 = o2
for f being Element of F₂() holds o1 . f = o2 . f

proof

let f be Element of F₂(); :: thesis: o1 . f = o2 . f
o1 . f = F₃(f) by A1
.= o2 . f by A2 ;
hence o1 . f = o2 . f ; :: thesis: verum

end;

hence o1 = o2 by FUNCT_2:113; :: thesis: verum