let V, A be set ; :: thesis: for loc being V -valued Function
for n0 being Nat holds <*(PP_inversion (factorial_inv (A,loc,n0))),(factorial_loop_body (A,loc)),(factorial_inv (A,loc,n0))*> is SFHT of (ND (V,A))
let loc be V -valued Function; :: thesis: for n0 being Nat holds <*(PP_inversion (factorial_inv (A,loc,n0))),(factorial_loop_body (A,loc)),(factorial_inv (A,loc,n0))*> is SFHT of (ND (V,A))
let n0 be Nat; :: thesis: <*(PP_inversion (factorial_inv (A,loc,n0))),(factorial_loop_body (A,loc)),(factorial_inv (A,loc,n0))*> is SFHT of (ND (V,A))
set D = ND (V,A);
set inv = factorial_inv (A,loc,n0);
set B = factorial_loop_body (A,loc);
set N = PP_inversion (factorial_inv (A,loc,n0));
for d being Element of ND (V,A) st d in dom (PP_inversion (factorial_inv (A,loc,n0))) & (PP_inversion (factorial_inv (A,loc,n0))) . d = TRUE & d in dom (factorial_loop_body (A,loc)) & (factorial_loop_body (A,loc)) . d in dom (factorial_inv (A,loc,n0)) holds
(factorial_inv (A,loc,n0)) . ((factorial_loop_body (A,loc)) . d) = TRUE by PARTPR_2:10;
then <*(PP_inversion (factorial_inv (A,loc,n0))),(factorial_loop_body (A,loc)),(factorial_inv (A,loc,n0))*> in SFHTs (ND (V,A)) ;
hence <*(PP_inversion (factorial_inv (A,loc,n0))),(factorial_loop_body (A,loc)),(factorial_inv (A,loc,n0))*> is SFHT of (ND (V,A)) ; :: thesis: verum