let v be Function; :: thesis: ( v tohilbval is Function & v tohilbperm is Function & proj1 (v tohilbval) = NAT & proj1 (v tohilbperm) = NAT )
set f = v tohilbval ;
set g = v tohilbperm ;
deffunc H₁( set ) -> set = dom ((v . $1) tohilb);
deffunc H₂( set ) -> set = (v . $1) tohilb ;
set ff = { [n,H₁(n)] where n is Element of NAT : S₁[n] } ;
set gg = { [n,H₂(n)] where n is Element of NAT : S₁[n] } ;
set N = { n where n is Element of NAT : S₁[n] } ;
B10: { [n,H₁(n)] where n is Element of NAT : S₁[n] } is Function from FOMODEL0:sch 3();
hence v tohilbval is Function ; :: thesis: ( v tohilbperm is Function & proj1 (v tohilbval) = NAT & proj1 (v tohilbperm) = NAT )
reconsider f = v tohilbval as Function by B10;
B11: { [n,H₂(n)] where n is Element of NAT : S₁[n] } is Function from FOMODEL0:sch 3();
hence v tohilbperm is Function ; :: thesis: ( proj1 (v tohilbval) = NAT & proj1 (v tohilbperm) = NAT )
reconsider g = v tohilbperm as Function by B11;
B0: f = { [n,H₁(n)] where n is Element of NAT : S₁[n] } ;
BB2: dom f = { n where n is Element of NAT : S₁[n] } from ALTCAT_2:sch 2(B0);
B1: g = { [n,H₂(n)] where n is Element of NAT : S₁[n] } ;
dom g = { n where n is Element of NAT : S₁[n] } from ALTCAT_2:sch 2(B1);
hence ( proj1 (v tohilbval) = NAT & proj1 (v tohilbperm) = NAT ) by BB2, FOMODEL0:74; :: thesis: verum