let f1, f2 be UnOp of Z; :: thesis: ( ( for q being FinSequence st q in Z holds
f1 . q = p ^ q ) & ( for q being FinSequence st q in Z holds
f2 . q = p ^ q ) implies f1 = f2 )
assume that
A1: for q being FinSequence st q in Z holds
f1 . q = p ^ q and
A2: for q being FinSequence st q in Z holds
f2 . q = p ^ q ; :: thesis: f1 = f2
for w being Element of Z holds f1 . w = f2 . w

proof

let w be Element of Z; :: thesis: f1 . w = f2 . w
f1 . w = p ^ w by A1
.= f2 . w by A2 ;
hence f1 . w = f2 . w ; :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:def 8; :: thesis: verum