let v be Function; :: thesis: ( v tohilbval is Function & v tohilbperm is Function & proj1 () = NAT & proj1 () = NAT )
set f = v tohilbval ;
set g = v tohilbperm ;
deffunc H1( set ) -> set = dom ((v . \$1) tohilb);
deffunc H2( set ) -> set = (v . \$1) tohilb ;
set ff = { [n,H1(n)] where n is Element of NAT : S1[n] } ;
set gg = { [n,H2(n)] where n is Element of NAT : S1[n] } ;
set N = { n where n is Element of NAT : S1[n] } ;
B10: { [n,H1(n)] where n is Element of NAT : S1[n] } is Function from hence v tohilbval is Function ; :: thesis: ( v tohilbperm is Function & proj1 () = NAT & proj1 () = NAT )
reconsider f = v tohilbval as Function by B10;
B11: { [n,H2(n)] where n is Element of NAT : S1[n] } is Function from hence v tohilbperm is Function ; :: thesis: ( proj1 () = NAT & proj1 () = NAT )
reconsider g = v tohilbperm as Function by B11;
B0: f = { [n,H1(n)] where n is Element of NAT : S1[n] } ;
BB2: dom f = { n where n is Element of NAT : S1[n] } from B1: g = { [n,H2(n)] where n is Element of NAT : S1[n] } ;
dom g = { n where n is Element of NAT : S1[n] } from hence ( proj1 () = NAT & proj1 () = NAT ) by ; :: thesis: verum