let f, g be UnOp of H1(F); ( ( for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds f . x = [(- (x `1_3)),(- (x `2_3)),(- (x `3_3))] ) & ( for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds g . x = [(- (x `1_3)),(- (x `2_3)),(- (x `3_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_3)),(- (x `2_3)),(- (x `3_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_3)),(- (x `2_3)),(- (x `3_3))]
; f = g
for x being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds f . x = g . x
hence
f = g
by FUNCT_2:63; verum