deffunc H₅( Nat) -> Element of [:INT,INT,INT:] = In (H₄($1),[:INT,INT,INT:]);
consider f being Function of NATPLUS,[:INT,INT,INT:] such that
A1: for x being Element of NATPLUS holds f . x = H₅(x) from FUNCT_2:sch 4();
take f ; :: thesis: for n being non zero Nat holds f . n = [(- 1),((- (5 * (n ^2))) - (2 * n)),((- (5 * n)) - 1)]
let n be non zero Nat; :: thesis: f . n = [(- 1),((- (5 * (n ^2))) - (2 * n)),((- (5 * n)) - 1)]
n in NATPLUS by NAT_LAT:def 6;
hence f . n = H₅(n) by A1
.= H₄(n) ;
:: thesis: verum