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_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))] ; :: 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_3)),(- (x `2_3)),(- (x `3_3))] by A2
.= g . x by A3 ; :: thesis: verum

end;

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