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

proof

let w be Element of Q; :: thesis: f1 . w = f2 . w
reconsider w = w as FinSequence ;
f1 . w = t ^ 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