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