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