let x be set ; :: thesis: for g being Function st x is Nat holds
( (g tohilbperm) . x = (g . x) tohilb & (g tohilbval) . x = dom ((g . x) tohilb) )
let g be Function; :: thesis: ( x is Nat implies ( (g tohilbperm) . x = (g . x) tohilb & (g tohilbval) . x = dom ((g . x) tohilb) ) )
set fv = g tohilbval ;
set fp = g tohilbperm ;
assume x is Nat ; :: thesis: ( (g tohilbperm) . x = (g . x) tohilb & (g tohilbval) . x = dom ((g . x) tohilb) )
then reconsider n = x as Element of NAT by ORDINAL1:def 12;
deffunc H₁( set ) -> set = (g . $1) tohilb ;
B0: S₁[n] ;
B1: g tohilbperm = { [o,H₁(o)] where o is Element of NAT : S₁[o] } ;
(g tohilbperm) . n = H₁(n) from ALTCAT_2:sch 3(B1, B0);
hence (g tohilbperm) . x = (g . x) tohilb ; :: thesis: (g tohilbval) . x = dom ((g . x) tohilb)
deffunc H₂( set ) -> set = dom H₁($1);
B2: g tohilbval = { [o,H₂(o)] where o is Element of NAT : S₁[o] } ;
(g tohilbval) . n = H₂(n) from ALTCAT_2:sch 3(B2, B0);
hence (g tohilbval) . x = dom ((g . x) tohilb) ; :: thesis: verum