deffunc H₂( Element of H₁(F)) -> Element of [:the carrier of F,the carrier of F,the carrier of F:] = [(- ($1 `1 )),(- ($1 `2 )),(- ($1 `3 ))];
consider f being UnOp of H<sub>1</sub>(F) such that
A1: for x being Element of [:the carrier of F,the carrier of F,the carrier of F:] holds f . x = H<sub>2</sub>(x) from FUNCT_2:sch 4();
take 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 ))]
thus 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 ))] by A1; :: thesis: verum