let V, A be set ; :: thesis: for loc being V -valued Function

for n0 being Nat st not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V & loc /. 1,loc /. 2,loc /. 3,loc /. 4 are_mutually_distinct holds

<*(factorial_inv (A,loc,n0)),(factorial_main_loop (A,loc)),(PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))))*> is SFHT of (ND (V,A))

let loc be V -valued Function; :: thesis: for n0 being Nat st not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V & loc /. 1,loc /. 2,loc /. 3,loc /. 4 are_mutually_distinct holds

<*(factorial_inv (A,loc,n0)),(factorial_main_loop (A,loc)),(PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))))*> is SFHT of (ND (V,A))

let n0 be Nat; :: thesis: ( not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V & loc /. 1,loc /. 2,loc /. 3,loc /. 4 are_mutually_distinct implies <*(factorial_inv (A,loc,n0)),(factorial_main_loop (A,loc)),(PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))))*> is SFHT of (ND (V,A)) )

set i = loc /. 1;

set j = loc /. 2;

set n = loc /. 3;

set s = loc /. 4;

set D = ND (V,A);

set inv = factorial_inv (A,loc,n0);

set B = factorial_loop_body (A,loc);

set E = Equality (A,(loc /. 1),(loc /. 3));

set N = PP_inversion (factorial_inv (A,loc,n0));

assume ( not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V & loc /. 1,loc /. 2,loc /. 3,loc /. 4 are_mutually_distinct ) ; :: thesis: <*(factorial_inv (A,loc,n0)),(factorial_main_loop (A,loc)),(PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))))*> is SFHT of (ND (V,A))

then A1: <*(factorial_inv (A,loc,n0)),(factorial_loop_body (A,loc)),(factorial_inv (A,loc,n0))*> is SFHT of (ND (V,A)) by Th7;

PP_and ((PP_not (Equality (A,(loc /. 1),(loc /. 3)))),(factorial_inv (A,loc,n0))) ||= factorial_inv (A,loc,n0) by NOMIN_3:3;

then A2: <*(PP_and ((PP_not (Equality (A,(loc /. 1),(loc /. 3)))),(factorial_inv (A,loc,n0)))),(factorial_loop_body (A,loc)),(factorial_inv (A,loc,n0))*> is SFHT of (ND (V,A)) by A1, NOMIN_3:15;

A3: <*(PP_inversion (factorial_inv (A,loc,n0))),(factorial_loop_body (A,loc)),(factorial_inv (A,loc,n0))*> is SFHT of (ND (V,A)) by NOMIN_3:19;

PP_and ((PP_not (Equality (A,(loc /. 1),(loc /. 3)))),(PP_inversion (factorial_inv (A,loc,n0)))) ||= PP_inversion (factorial_inv (A,loc,n0)) by NOMIN_3:3;

then <*(PP_and ((PP_not (Equality (A,(loc /. 1),(loc /. 3)))),(PP_inversion (factorial_inv (A,loc,n0))))),(factorial_loop_body (A,loc)),(factorial_inv (A,loc,n0))*> is SFHT of (ND (V,A)) by A3, NOMIN_3:15;

hence <*(factorial_inv (A,loc,n0)),(factorial_main_loop (A,loc)),(PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))))*> is SFHT of (ND (V,A)) by A2, NOMIN_3:26; :: thesis: verum

for n0 being Nat st not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V & loc /. 1,loc /. 2,loc /. 3,loc /. 4 are_mutually_distinct holds

<*(factorial_inv (A,loc,n0)),(factorial_main_loop (A,loc)),(PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))))*> is SFHT of (ND (V,A))

let loc be V -valued Function; :: thesis: for n0 being Nat st not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V & loc /. 1,loc /. 2,loc /. 3,loc /. 4 are_mutually_distinct holds

<*(factorial_inv (A,loc,n0)),(factorial_main_loop (A,loc)),(PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))))*> is SFHT of (ND (V,A))

let n0 be Nat; :: thesis: ( not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V & loc /. 1,loc /. 2,loc /. 3,loc /. 4 are_mutually_distinct implies <*(factorial_inv (A,loc,n0)),(factorial_main_loop (A,loc)),(PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))))*> is SFHT of (ND (V,A)) )

set i = loc /. 1;

set j = loc /. 2;

set n = loc /. 3;

set s = loc /. 4;

set D = ND (V,A);

set inv = factorial_inv (A,loc,n0);

set B = factorial_loop_body (A,loc);

set E = Equality (A,(loc /. 1),(loc /. 3));

set N = PP_inversion (factorial_inv (A,loc,n0));

assume ( not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V & loc /. 1,loc /. 2,loc /. 3,loc /. 4 are_mutually_distinct ) ; :: thesis: <*(factorial_inv (A,loc,n0)),(factorial_main_loop (A,loc)),(PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))))*> is SFHT of (ND (V,A))

then A1: <*(factorial_inv (A,loc,n0)),(factorial_loop_body (A,loc)),(factorial_inv (A,loc,n0))*> is SFHT of (ND (V,A)) by Th7;

PP_and ((PP_not (Equality (A,(loc /. 1),(loc /. 3)))),(factorial_inv (A,loc,n0))) ||= factorial_inv (A,loc,n0) by NOMIN_3:3;

then A2: <*(PP_and ((PP_not (Equality (A,(loc /. 1),(loc /. 3)))),(factorial_inv (A,loc,n0)))),(factorial_loop_body (A,loc)),(factorial_inv (A,loc,n0))*> is SFHT of (ND (V,A)) by A1, NOMIN_3:15;

A3: <*(PP_inversion (factorial_inv (A,loc,n0))),(factorial_loop_body (A,loc)),(factorial_inv (A,loc,n0))*> is SFHT of (ND (V,A)) by NOMIN_3:19;

PP_and ((PP_not (Equality (A,(loc /. 1),(loc /. 3)))),(PP_inversion (factorial_inv (A,loc,n0)))) ||= PP_inversion (factorial_inv (A,loc,n0)) by NOMIN_3:3;

then <*(PP_and ((PP_not (Equality (A,(loc /. 1),(loc /. 3)))),(PP_inversion (factorial_inv (A,loc,n0))))),(factorial_loop_body (A,loc)),(factorial_inv (A,loc,n0))*> is SFHT of (ND (V,A)) by A3, NOMIN_3:15;

hence <*(factorial_inv (A,loc,n0)),(factorial_main_loop (A,loc)),(PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))))*> is SFHT of (ND (V,A)) by A2, NOMIN_3:26; :: thesis: verum