let V, A be set ; :: thesis: for loc being V -valued Function
for n0 being Nat
for b0 being Complex st not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V & loc /. 1,loc /. 2,loc /. 3,loc /. 4,loc /. 5 are_mutually_distinct holds
<*(power_inv (A,loc,b0,n0)),(power_main_loop (A,loc)),(PP_and ((Equality (A,(loc /. 1),(loc /. 4))),(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 st not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V & loc /. 1,loc /. 2,loc /. 3,loc /. 4,loc /. 5 are_mutually_distinct holds
<*(power_inv (A,loc,b0,n0)),(power_main_loop (A,loc)),(PP_and ((Equality (A,(loc /. 1),(loc /. 4))),(power_inv (A,loc,b0,n0))))*> is SFHT of (ND (V,A))
let n0 be Nat; :: thesis: for b0 being Complex st not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V & loc /. 1,loc /. 2,loc /. 3,loc /. 4,loc /. 5 are_mutually_distinct holds
<*(power_inv (A,loc,b0,n0)),(power_main_loop (A,loc)),(PP_and ((Equality (A,(loc /. 1),(loc /. 4))),(power_inv (A,loc,b0,n0))))*> is SFHT of (ND (V,A))
let b0 be Complex; :: thesis: ( not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V & loc /. 1,loc /. 2,loc /. 3,loc /. 4,loc /. 5 are_mutually_distinct implies <*(power_inv (A,loc,b0,n0)),(power_main_loop (A,loc)),(PP_and ((Equality (A,(loc /. 1),(loc /. 4))),(power_inv (A,loc,b0,n0))))*> is SFHT of (ND (V,A)) )
set i = loc /. 1;
set j = loc /. 2;
set b = loc /. 3;
set n = loc /. 4;
set s = loc /. 5;
set D = ND (V,A);
set inv = power_inv (A,loc,b0,n0);
set B = power_loop_body (A,loc);
set E = Equality (A,(loc /. 1),(loc /. 4));
assume ( not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V & loc /. 1,loc /. 2,loc /. 3,loc /. 4,loc /. 5 are_mutually_distinct ) ; :: thesis: <*(power_inv (A,loc,b0,n0)),(power_main_loop (A,loc)),(PP_and ((Equality (A,(loc /. 1),(loc /. 4))),(power_inv (A,loc,b0,n0))))*> is SFHT of (ND (V,A))
then A1: <*(power_inv (A,loc,b0,n0)),(power_loop_body (A,loc)),(power_inv (A,loc,b0,n0))*> is SFHT of (ND (V,A)) by Th5;
PP_and ((PP_not (Equality (A,(loc /. 1),(loc /. 4)))),(power_inv (A,loc,b0,n0))) ||= power_inv (A,loc,b0,n0) by NOMIN_3:3;
then A2: <*(PP_and ((PP_not (Equality (A,(loc /. 1),(loc /. 4)))),(power_inv (A,loc,b0,n0)))),(power_loop_body (A,loc)),(power_inv (A,loc,b0,n0))*> is SFHT of (ND (V,A)) by A1, NOMIN_3:15;
A3: <*(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)) by NOMIN_3:19;
PP_and ((PP_not (Equality (A,(loc /. 1),(loc /. 4)))),(PP_inversion (power_inv (A,loc,b0,n0)))) ||= PP_inversion (power_inv (A,loc,b0,n0)) by NOMIN_3:3;
then <*(PP_and ((PP_not (Equality (A,(loc /. 1),(loc /. 4)))),(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)) by A3, NOMIN_3:15;
hence <*(power_inv (A,loc,b0,n0)),(power_main_loop (A,loc)),(PP_and ((Equality (A,(loc /. 1),(loc /. 4))),(power_inv (A,loc,b0,n0))))*> is SFHT of (ND (V,A)) by A2, NOMIN_3:26; :: thesis: verum