set X = the carrier of AFV;
let o1, o2 be UnOp of the carrier of AFV; :: thesis: ( ( for a being Element of AFV holds o1 . a = Pcom (o,a) ) & ( for a being Element of AFV holds o2 . a = Pcom (o,a) ) implies o1 = o2 )
assume that
A2: for a being Element of AFV holds o1 . a = Pcom (o,a) and
A3: for a being Element of AFV holds o2 . a = Pcom (o,a) ; :: thesis: o1 = o2
for x being Element of the carrier of AFV holds o1 . x = o2 . x

proof

let x be Element of the carrier of AFV; :: thesis: o1 . x = o2 . x
o1 . x = Pcom (o,x) by A2
.= o2 . x by A3 ;
hence o1 . x = o2 . x ; :: thesis: verum

end;

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