let V, A be set ; :: thesis: for loc being V -valued Function
for val being 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 & loc,val are_compatible_wrt_4_locs holds
<*(valid_factorial_input (V,A,val,n0)),(factorial_main_part (A,loc,val)),(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 val being 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 & loc,val are_compatible_wrt_4_locs holds
<*(valid_factorial_input (V,A,val,n0)),(factorial_main_part (A,loc,val)),(PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))))*> is SFHT of (ND (V,A))
let val be 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 & loc,val are_compatible_wrt_4_locs holds
<*(valid_factorial_input (V,A,val,n0)),(factorial_main_part (A,loc,val)),(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 & loc,val are_compatible_wrt_4_locs implies <*(valid_factorial_input (V,A,val,n0)),(factorial_main_part (A,loc,val)),(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 i1 = val . 1;
set j1 = val . 2;
set n1 = val . 3;
set s1 = val . 4;
set D = ND (V,A);
set p = valid_factorial_input (V,A,val,n0);
set f = factorial_var_init (A,loc,val);
set g = factorial_main_loop (A,loc);
set q = factorial_inv (A,loc,n0);
set r = PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0)));
assume A1: ( 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 & loc,val are_compatible_wrt_4_locs ) ; :: thesis: <*(valid_factorial_input (V,A,val,n0)),(factorial_main_part (A,loc,val)),(PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))))*> is SFHT of (ND (V,A))
then A2: <*(valid_factorial_input (V,A,val,n0)),(factorial_var_init (A,loc,val)),(factorial_inv (A,loc,n0))*> is SFHT of (ND (V,A)) by Th6;
A3: <*(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 A1, Th9;
<*(PP_inversion (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 NOMIN_3:19;
hence <*(valid_factorial_input (V,A,val,n0)),(factorial_main_part (A,loc,val)),(PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))))*> is SFHT of (ND (V,A)) by A2, A3, NOMIN_3:25; :: thesis: verum