deffunc H₂( Element of H₁(F)) -> Element of [: the carrier of F, the carrier of F, the carrier of F:] = [(- ($1 `1_3)),(- ($1 `2_3)),(- ($1 `3_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_3)),(- (x `2_3)),(- (x `3_3))]
thus 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))] by A1; :: thesis: verum