let f, g be UnOp of H₁(F); :: thesis: ( ( for x being Element of [:the carrier of F,the carrier of F,the carrier of F:] holds f . x = [(- (x `1 )),(- (x `2 )),(- (x `3 ))] ) & ( for x being Element of [:the carrier of F,the carrier of F,the carrier of F:] holds g . x = [(- (x `1 )),(- (x `2 )),(- (x `3 ))] ) implies f = g )
assume that
A2: for x being Element of [:the carrier of F,the carrier of F,the carrier of F:] holds f . x = [(- (x `1 )),(- (x `2 )),(- (x `3 ))] and
A3: for x being Element of [:the carrier of F,the carrier of F,the carrier of F:] holds g . x = [(- (x `1 )),(- (x `2 )),(- (x `3 ))] ; :: thesis: f = g
for x being Element of [:the carrier of F,the carrier of F,the carrier of F:] holds f . x = g . x

proof

let x be Element of [:the carrier of F,the carrier of F,the carrier of F:]; :: thesis: f . x = g . x
thus f . x = [(- (x `1 )),(- (x `2 )),(- (x `3 ))] by A2
.= g . x by A3 ; :: thesis: verum

end;

hence f = g by FUNCT_2:113; :: thesis: verum