deffunc H₆( Nat) -> Element of [:INT,INT,INT,INT:] = In (H₅($1),[:INT,INT,INT,INT:]);
consider f being Function of NAT,[:INT,INT,INT,INT:] such that
A1: for x being Element of NAT holds f . x = H₆(x) from FUNCT_2:sch 4();
take f ; :: thesis: for n being Nat holds f . n = [(- 1),n,(1 - n),(- 1)]
let n be Nat; :: thesis: f . n = [(- 1),n,(1 - n),(- 1)]
n in NAT by ORDINAL1:def 12;
hence f . n = H₆(n) by A1
.= H₅(n) ;
:: thesis: verum