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_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_var_init (A,loc,val)),(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_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_var_init (A,loc,val)),(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_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_var_init (A,loc,val)),(factorial_inv (A,loc,n0))*> is SFHT of (ND (V,A))

let n0 be Nat; :: thesis: ( not V is empty & 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_var_init (A,loc,val)),(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 I = valid_factorial_input (V,A,val,n0);

set F = factorial_var_init (A,loc,val);

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

set Di = denaming (V,A,(val . 1));

set Dj = denaming (V,A,(val . 2));

set Dn = denaming (V,A,(val . 3));

set Ds = denaming (V,A,(val . 4));

set asi = SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1));

set asj = SC_assignment ((denaming (V,A,(val . 2))),(loc /. 2));

set asn = SC_assignment ((denaming (V,A,(val . 3))),(loc /. 3));

set ass = SC_assignment ((denaming (V,A,(val . 4))),(loc /. 4));

set S1 = SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4));

set R1 = SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3));

set Q1 = SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2));

set P1 = SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1));

assume that

A1: not V is empty and

A2: A is_without_nonatomicND_wrt V and

A3: loc /. 1,loc /. 2,loc /. 3,loc /. 4 are_mutually_distinct and

A4: loc,val are_compatible_wrt_4_locs ; :: thesis: <*(valid_factorial_input (V,A,val,n0)),(factorial_var_init (A,loc,val)),(factorial_inv (A,loc,n0))*> is SFHT of (ND (V,A))

A5: <*(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(SC_assignment ((denaming (V,A,(val . 2))),(loc /. 2))),(SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3)))*> is SFHT of (ND (V,A)) by NOMIN_3:29;

A6: <*(SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(SC_assignment ((denaming (V,A,(val . 3))),(loc /. 3))),(SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4)))*> is SFHT of (ND (V,A)) by NOMIN_3:29;

A7: <*(SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(SC_assignment ((denaming (V,A,(val . 4))),(loc /. 4))),(factorial_inv (A,loc,n0))*> is SFHT of (ND (V,A)) by NOMIN_3:29;

A8: <*(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))),(SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1))),(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2)))*> is SFHT of (ND (V,A)) by NOMIN_3:29;

valid_factorial_input (V,A,val,n0) ||= SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))

A63: <*(PP_inversion (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2)))),(SC_assignment ((denaming (V,A,(val . 2))),(loc /. 2))),(SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3)))*> is SFHT of (ND (V,A)) by NOMIN_4:16;

A64: <*(PP_inversion (SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3)))),(SC_assignment ((denaming (V,A,(val . 3))),(loc /. 3))),(SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4)))*> is SFHT of (ND (V,A)) by NOMIN_4:16;

<*(PP_inversion (SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4)))),(SC_assignment ((denaming (V,A,(val . 4))),(loc /. 4))),(factorial_inv (A,loc,n0))*> is SFHT of (ND (V,A)) by NOMIN_4:16;

hence <*(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 A62, A5, A6, A7, A63, A64, Th2; :: thesis: verum

for val being Function

for n0 being Nat st not V is empty & 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_var_init (A,loc,val)),(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_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_var_init (A,loc,val)),(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_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_var_init (A,loc,val)),(factorial_inv (A,loc,n0))*> is SFHT of (ND (V,A))

let n0 be Nat; :: thesis: ( not V is empty & 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_var_init (A,loc,val)),(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 I = valid_factorial_input (V,A,val,n0);

set F = factorial_var_init (A,loc,val);

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

set Di = denaming (V,A,(val . 1));

set Dj = denaming (V,A,(val . 2));

set Dn = denaming (V,A,(val . 3));

set Ds = denaming (V,A,(val . 4));

set asi = SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1));

set asj = SC_assignment ((denaming (V,A,(val . 2))),(loc /. 2));

set asn = SC_assignment ((denaming (V,A,(val . 3))),(loc /. 3));

set ass = SC_assignment ((denaming (V,A,(val . 4))),(loc /. 4));

set S1 = SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4));

set R1 = SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3));

set Q1 = SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2));

set P1 = SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1));

assume that

A1: not V is empty and

A2: A is_without_nonatomicND_wrt V and

A3: loc /. 1,loc /. 2,loc /. 3,loc /. 4 are_mutually_distinct and

A4: loc,val are_compatible_wrt_4_locs ; :: thesis: <*(valid_factorial_input (V,A,val,n0)),(factorial_var_init (A,loc,val)),(factorial_inv (A,loc,n0))*> is SFHT of (ND (V,A))

A5: <*(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(SC_assignment ((denaming (V,A,(val . 2))),(loc /. 2))),(SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3)))*> is SFHT of (ND (V,A)) by NOMIN_3:29;

A6: <*(SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(SC_assignment ((denaming (V,A,(val . 3))),(loc /. 3))),(SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4)))*> is SFHT of (ND (V,A)) by NOMIN_3:29;

A7: <*(SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(SC_assignment ((denaming (V,A,(val . 4))),(loc /. 4))),(factorial_inv (A,loc,n0))*> is SFHT of (ND (V,A)) by NOMIN_3:29;

A8: <*(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))),(SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1))),(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2)))*> is SFHT of (ND (V,A)) by NOMIN_3:29;

valid_factorial_input (V,A,val,n0) ||= SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))

proof

then A62:
<*(valid_factorial_input (V,A,val,n0)),(SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1))),(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2)))*> is SFHT of (ND (V,A))
by A8, NOMIN_3:15;
let d be Element of ND (V,A); :: according to NOMIN_3:def 3 :: thesis: ( not d in dom (valid_factorial_input (V,A,val,n0)) or not (valid_factorial_input (V,A,val,n0)) . d = TRUE or ( d in dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))) & (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))) . d = TRUE ) )

assume ( d in dom (valid_factorial_input (V,A,val,n0)) & (valid_factorial_input (V,A,val,n0)) . d = TRUE ) ; :: thesis: ( d in dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))) & (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))) . d = TRUE )

then valid_factorial_input_pred V,A,val,n0,d by Def15;

then consider d1 being NonatomicND of V,A such that

A9: d = d1 and

A10: {(val . 1),(val . 2),(val . 3),(val . 4)} c= dom d1 and

A11: d1 . (val . 1) = 0 and

A12: d1 . (val . 2) = 1 and

A13: d1 . (val . 3) = n0 and

A14: d1 . (val . 4) = 1 ;

A15: val . 1 in {(val . 1),(val . 2),(val . 3),(val . 4)} by ENUMSET1:def 2;

A16: val . 2 in {(val . 1),(val . 2),(val . 3),(val . 4)} by ENUMSET1:def 2;

A17: val . 3 in {(val . 1),(val . 2),(val . 3),(val . 4)} by ENUMSET1:def 2;

A18: val . 4 in {(val . 1),(val . 2),(val . 3),(val . 4)} by ENUMSET1:def 2;

A20: dom (denaming (V,A,(val . 1))) = { d where d is NonatomicND of V,A : val . 1 in dom d } by NOMIN_1:def 18;

A21: dom (denaming (V,A,(val . 2))) = { d where d is NonatomicND of V,A : val . 2 in dom d } by NOMIN_1:def 18;

A22: dom (denaming (V,A,(val . 3))) = { d where d is NonatomicND of V,A : val . 3 in dom d } by NOMIN_1:def 18;

A23: dom (denaming (V,A,(val . 4))) = { d where d is NonatomicND of V,A : val . 4 in dom d } by NOMIN_1:def 18;

A24: dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,(val . 1))) . d),(loc /. 1)) in dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))) & d in dom (denaming (V,A,(val . 1))) ) } by NOMIN_2:def 11;

A25: dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,(val . 2))) . d),(loc /. 2)) in dom (SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))) & d in dom (denaming (V,A,(val . 2))) ) } by NOMIN_2:def 11;

A26: dom (SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,(val . 3))) . d),(loc /. 3)) in dom (SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))) & d in dom (denaming (V,A,(val . 3))) ) } by NOMIN_2:def 11;

A27: dom (SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,(val . 4))) . d),(loc /. 4)) in dom (factorial_inv (A,loc,n0)) & d in dom (denaming (V,A,(val . 4))) ) } by NOMIN_2:def 11;

reconsider Li = local_overlapping (V,A,d1,((denaming (V,A,(val . 1))) . d1),(loc /. 1)) as NonatomicND of V,A by NOMIN_2:9;

reconsider Lj = local_overlapping (V,A,Li,((denaming (V,A,(val . 2))) . Li),(loc /. 2)) as NonatomicND of V,A by NOMIN_2:9;

reconsider Ln = local_overlapping (V,A,Lj,((denaming (V,A,(val . 3))) . Lj),(loc /. 3)) as NonatomicND of V,A by NOMIN_2:9;

reconsider Ls = local_overlapping (V,A,Ln,((denaming (V,A,(val . 4))) . Ln),(loc /. 4)) as NonatomicND of V,A by NOMIN_2:9;

A28: d1 in dom (denaming (V,A,(val . 1))) by A10, A15, A20;

then A29: (denaming (V,A,(val . 1))) . d1 is TypeSCNominativeData of V,A by PARTFUN1:4, NOMIN_1:39;

then A30: dom Li = {(loc /. 1)} \/ (dom d1) by A1, A2, NOMIN_4:4;

dom (factorial_inv (A,loc,n0)) = ND (V,A) by Def19;

then A31: Ls in dom (factorial_inv (A,loc,n0)) ;

A32: val . 2 in dom Li by A10, A16, A30, XBOOLE_0:def 3;

then A33: Li in dom (denaming (V,A,(val . 2))) by A21;

then A34: (denaming (V,A,(val . 2))) . Li is TypeSCNominativeData of V,A by PARTFUN1:4, NOMIN_1:39;

then A35: dom Lj = {(loc /. 2)} \/ (dom Li) by A1, A2, NOMIN_4:4;

A36: val . 3 in dom Li by A10, A17, A30, XBOOLE_0:def 3;

then A37: val . 3 in dom Lj by A35, XBOOLE_0:def 3;

then A38: Lj in dom (denaming (V,A,(val . 3))) by A22;

then A39: (denaming (V,A,(val . 3))) . Lj is TypeSCNominativeData of V,A by PARTFUN1:4, NOMIN_1:39;

then A40: dom Ln = {(loc /. 3)} \/ (dom Lj) by A1, A2, NOMIN_4:4;

A41: val . 4 in dom Li by A10, A18, A30, XBOOLE_0:def 3;

then A42: val . 4 in dom Lj by A35, XBOOLE_0:def 3;

then A43: val . 4 in dom Ln by A40, XBOOLE_0:def 3;

then A44: Ln in dom (denaming (V,A,(val . 4))) by A23;

then A45: Ln in dom (SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))) by A27, A31;

A46: Lj in dom (SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))) by A26, A45, A38;

then A47: Li in dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))) by A25, A33;

hence A48: d in dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))) by A9, A24, A28; :: thesis: (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))) . d = TRUE

A49: factorial_inv_pred A,loc,n0,Ls

.= (SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))) . Lj by A47, NOMIN_2:35

.= (SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))) . Ln by A46, NOMIN_2:35

.= (factorial_inv (A,loc,n0)) . Ls by A45, NOMIN_2:35

.= TRUE by A31, A49, Def19 ; :: thesis: verum

end;assume ( d in dom (valid_factorial_input (V,A,val,n0)) & (valid_factorial_input (V,A,val,n0)) . d = TRUE ) ; :: thesis: ( d in dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))) & (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))) . d = TRUE )

then valid_factorial_input_pred V,A,val,n0,d by Def15;

then consider d1 being NonatomicND of V,A such that

A9: d = d1 and

A10: {(val . 1),(val . 2),(val . 3),(val . 4)} c= dom d1 and

A11: d1 . (val . 1) = 0 and

A12: d1 . (val . 2) = 1 and

A13: d1 . (val . 3) = n0 and

A14: d1 . (val . 4) = 1 ;

A15: val . 1 in {(val . 1),(val . 2),(val . 3),(val . 4)} by ENUMSET1:def 2;

A16: val . 2 in {(val . 1),(val . 2),(val . 3),(val . 4)} by ENUMSET1:def 2;

A17: val . 3 in {(val . 1),(val . 2),(val . 3),(val . 4)} by ENUMSET1:def 2;

A18: val . 4 in {(val . 1),(val . 2),(val . 3),(val . 4)} by ENUMSET1:def 2;

A20: dom (denaming (V,A,(val . 1))) = { d where d is NonatomicND of V,A : val . 1 in dom d } by NOMIN_1:def 18;

A21: dom (denaming (V,A,(val . 2))) = { d where d is NonatomicND of V,A : val . 2 in dom d } by NOMIN_1:def 18;

A22: dom (denaming (V,A,(val . 3))) = { d where d is NonatomicND of V,A : val . 3 in dom d } by NOMIN_1:def 18;

A23: dom (denaming (V,A,(val . 4))) = { d where d is NonatomicND of V,A : val . 4 in dom d } by NOMIN_1:def 18;

A24: dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,(val . 1))) . d),(loc /. 1)) in dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))) & d in dom (denaming (V,A,(val . 1))) ) } by NOMIN_2:def 11;

A25: dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,(val . 2))) . d),(loc /. 2)) in dom (SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))) & d in dom (denaming (V,A,(val . 2))) ) } by NOMIN_2:def 11;

A26: dom (SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,(val . 3))) . d),(loc /. 3)) in dom (SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))) & d in dom (denaming (V,A,(val . 3))) ) } by NOMIN_2:def 11;

A27: dom (SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,(val . 4))) . d),(loc /. 4)) in dom (factorial_inv (A,loc,n0)) & d in dom (denaming (V,A,(val . 4))) ) } by NOMIN_2:def 11;

reconsider Li = local_overlapping (V,A,d1,((denaming (V,A,(val . 1))) . d1),(loc /. 1)) as NonatomicND of V,A by NOMIN_2:9;

reconsider Lj = local_overlapping (V,A,Li,((denaming (V,A,(val . 2))) . Li),(loc /. 2)) as NonatomicND of V,A by NOMIN_2:9;

reconsider Ln = local_overlapping (V,A,Lj,((denaming (V,A,(val . 3))) . Lj),(loc /. 3)) as NonatomicND of V,A by NOMIN_2:9;

reconsider Ls = local_overlapping (V,A,Ln,((denaming (V,A,(val . 4))) . Ln),(loc /. 4)) as NonatomicND of V,A by NOMIN_2:9;

A28: d1 in dom (denaming (V,A,(val . 1))) by A10, A15, A20;

then A29: (denaming (V,A,(val . 1))) . d1 is TypeSCNominativeData of V,A by PARTFUN1:4, NOMIN_1:39;

then A30: dom Li = {(loc /. 1)} \/ (dom d1) by A1, A2, NOMIN_4:4;

dom (factorial_inv (A,loc,n0)) = ND (V,A) by Def19;

then A31: Ls in dom (factorial_inv (A,loc,n0)) ;

A32: val . 2 in dom Li by A10, A16, A30, XBOOLE_0:def 3;

then A33: Li in dom (denaming (V,A,(val . 2))) by A21;

then A34: (denaming (V,A,(val . 2))) . Li is TypeSCNominativeData of V,A by PARTFUN1:4, NOMIN_1:39;

then A35: dom Lj = {(loc /. 2)} \/ (dom Li) by A1, A2, NOMIN_4:4;

A36: val . 3 in dom Li by A10, A17, A30, XBOOLE_0:def 3;

then A37: val . 3 in dom Lj by A35, XBOOLE_0:def 3;

then A38: Lj in dom (denaming (V,A,(val . 3))) by A22;

then A39: (denaming (V,A,(val . 3))) . Lj is TypeSCNominativeData of V,A by PARTFUN1:4, NOMIN_1:39;

then A40: dom Ln = {(loc /. 3)} \/ (dom Lj) by A1, A2, NOMIN_4:4;

A41: val . 4 in dom Li by A10, A18, A30, XBOOLE_0:def 3;

then A42: val . 4 in dom Lj by A35, XBOOLE_0:def 3;

then A43: val . 4 in dom Ln by A40, XBOOLE_0:def 3;

then A44: Ln in dom (denaming (V,A,(val . 4))) by A23;

then A45: Ln in dom (SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))) by A27, A31;

A46: Lj in dom (SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))) by A26, A45, A38;

then A47: Li in dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))) by A25, A33;

hence A48: d in dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))) by A9, A24, A28; :: thesis: (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))) . d = TRUE

A49: factorial_inv_pred A,loc,n0,Ls

proof

thus (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))) . d =
(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))) . Li
by A9, A48, NOMIN_2:35
take
Ls
; :: according to NOMIN_5:def 18 :: thesis: ( Ls = Ls & {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4)} c= dom Ls & Ls . (loc /. 2) = 1 & Ls . (loc /. 3) = n0 & ex I, S being Nat st

( I = Ls . (loc /. 1) & S = Ls . (loc /. 4) & S = I ! ) )

thus Ls = Ls ; :: thesis: ( {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4)} c= dom Ls & Ls . (loc /. 2) = 1 & Ls . (loc /. 3) = n0 & ex I, S being Nat st

( I = Ls . (loc /. 1) & S = Ls . (loc /. 4) & S = I ! ) )

A50: (denaming (V,A,(val . 4))) . Ln is TypeSCNominativeData of V,A by A44, PARTFUN1:4, NOMIN_1:39;

then A51: dom Ls = {(loc /. 4)} \/ (dom Ln) by A1, A2, NOMIN_4:4;

loc /. 1 in {(loc /. 1)} by TARSKI:def 1;

then A52: loc /. 1 in dom Li by A30, XBOOLE_0:def 3;

then A53: loc /. 1 in dom Lj by A35, XBOOLE_0:def 3;

then A54: loc /. 1 in dom Ln by A40, XBOOLE_0:def 3;

then A55: loc /. 1 in dom Ls by A51, XBOOLE_0:def 3;

loc /. 2 in {(loc /. 2)} by TARSKI:def 1;

then A56: loc /. 2 in dom Lj by A35, XBOOLE_0:def 3;

then A57: loc /. 2 in dom Ln by A40, XBOOLE_0:def 3;

then A58: loc /. 2 in dom Ls by A51, XBOOLE_0:def 3;

loc /. 3 in {(loc /. 3)} by TARSKI:def 1;

then A59: loc /. 3 in dom Ln by A40, XBOOLE_0:def 3;

then A60: loc /. 3 in dom Ls by A51, XBOOLE_0:def 3;

loc /. 4 in {(loc /. 4)} by TARSKI:def 1;

then loc /. 4 in dom Ls by A51, XBOOLE_0:def 3;

hence {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4)} c= dom Ls by A55, A58, A60, ENUMSET1:def 2; :: thesis: ( Ls . (loc /. 2) = 1 & Ls . (loc /. 3) = n0 & ex I, S being Nat st

( I = Ls . (loc /. 1) & S = Ls . (loc /. 4) & S = I ! ) )

thus Ls . (loc /. 2) = Ln . (loc /. 2) by A1, A2, A3, A50, A57, Th3

.= Lj . (loc /. 2) by A1, A2, A3, A39, A56, Th3

.= (denaming (V,A,(val . 2))) . Li by A1, A34, NOMIN_2:10

.= denaming ((val . 2),Li) by A33, NOMIN_1:def 18

.= Li . (val . 2) by A32, NOMIN_1:def 12

.= 1 by A1, A2, A4, A10, A16, A12, A29, Th3 ; :: thesis: ( Ls . (loc /. 3) = n0 & ex I, S being Nat st

( I = Ls . (loc /. 1) & S = Ls . (loc /. 4) & S = I ! ) )

thus Ls . (loc /. 3) = Ln . (loc /. 3) by A1, A2, A3, A50, A59, Th3

.= (denaming (V,A,(val . 3))) . Lj by A1, A39, NOMIN_2:10

.= denaming ((val . 3),Lj) by A38, NOMIN_1:def 18

.= Lj . (val . 3) by A37, NOMIN_1:def 12

.= Li . (val . 3) by A1, A2, A4, A34, A36, Th3

.= n0 by A1, A2, A4, A10, A17, A13, A29, Th3 ; :: thesis: ex I, S being Nat st

( I = Ls . (loc /. 1) & S = Ls . (loc /. 4) & S = I ! )

A61: Ln . (val . 4) = Lj . (val . 4) by A1, A2, A4, A42, A39, Th3

.= Li . (val . 4) by A1, A2, A4, A34, A41, Th3

.= 1 by A1, A2, A4, A10, A18, A14, A29, Th3 ;

take 0 ; :: thesis: ex S being Nat st

( 0 = Ls . (loc /. 1) & S = Ls . (loc /. 4) & S = 0 ! )

take 1 ; :: thesis: ( 0 = Ls . (loc /. 1) & 1 = Ls . (loc /. 4) & 1 = 0 ! )

thus Ls . (loc /. 1) = Ln . (loc /. 1) by A1, A2, A3, A50, A54, Th3

.= Lj . (loc /. 1) by A1, A2, A3, A53, A39, Th3

.= Li . (loc /. 1) by A1, A2, A3, A34, A52, Th3

.= (denaming (V,A,(val . 1))) . d1 by A1, A29, NOMIN_2:10

.= denaming ((val . 1),d1) by A28, NOMIN_1:def 18

.= 0 by A10, A11, A15, NOMIN_1:def 12 ; :: thesis: ( 1 = Ls . (loc /. 4) & 1 = 0 ! )

thus Ls . (loc /. 4) = (denaming (V,A,(val . 4))) . Ln by A1, A50, NOMIN_2:10

.= denaming ((val . 4),Ln) by A44, NOMIN_1:def 18

.= 1 by A61, A43, NOMIN_1:def 12 ; :: thesis: 1 = 0 !

thus 1 = 0 ! by NEWTON:12; :: thesis: verum

end;( I = Ls . (loc /. 1) & S = Ls . (loc /. 4) & S = I ! ) )

thus Ls = Ls ; :: thesis: ( {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4)} c= dom Ls & Ls . (loc /. 2) = 1 & Ls . (loc /. 3) = n0 & ex I, S being Nat st

( I = Ls . (loc /. 1) & S = Ls . (loc /. 4) & S = I ! ) )

A50: (denaming (V,A,(val . 4))) . Ln is TypeSCNominativeData of V,A by A44, PARTFUN1:4, NOMIN_1:39;

then A51: dom Ls = {(loc /. 4)} \/ (dom Ln) by A1, A2, NOMIN_4:4;

loc /. 1 in {(loc /. 1)} by TARSKI:def 1;

then A52: loc /. 1 in dom Li by A30, XBOOLE_0:def 3;

then A53: loc /. 1 in dom Lj by A35, XBOOLE_0:def 3;

then A54: loc /. 1 in dom Ln by A40, XBOOLE_0:def 3;

then A55: loc /. 1 in dom Ls by A51, XBOOLE_0:def 3;

loc /. 2 in {(loc /. 2)} by TARSKI:def 1;

then A56: loc /. 2 in dom Lj by A35, XBOOLE_0:def 3;

then A57: loc /. 2 in dom Ln by A40, XBOOLE_0:def 3;

then A58: loc /. 2 in dom Ls by A51, XBOOLE_0:def 3;

loc /. 3 in {(loc /. 3)} by TARSKI:def 1;

then A59: loc /. 3 in dom Ln by A40, XBOOLE_0:def 3;

then A60: loc /. 3 in dom Ls by A51, XBOOLE_0:def 3;

loc /. 4 in {(loc /. 4)} by TARSKI:def 1;

then loc /. 4 in dom Ls by A51, XBOOLE_0:def 3;

hence {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4)} c= dom Ls by A55, A58, A60, ENUMSET1:def 2; :: thesis: ( Ls . (loc /. 2) = 1 & Ls . (loc /. 3) = n0 & ex I, S being Nat st

( I = Ls . (loc /. 1) & S = Ls . (loc /. 4) & S = I ! ) )

thus Ls . (loc /. 2) = Ln . (loc /. 2) by A1, A2, A3, A50, A57, Th3

.= Lj . (loc /. 2) by A1, A2, A3, A39, A56, Th3

.= (denaming (V,A,(val . 2))) . Li by A1, A34, NOMIN_2:10

.= denaming ((val . 2),Li) by A33, NOMIN_1:def 18

.= Li . (val . 2) by A32, NOMIN_1:def 12

.= 1 by A1, A2, A4, A10, A16, A12, A29, Th3 ; :: thesis: ( Ls . (loc /. 3) = n0 & ex I, S being Nat st

( I = Ls . (loc /. 1) & S = Ls . (loc /. 4) & S = I ! ) )

thus Ls . (loc /. 3) = Ln . (loc /. 3) by A1, A2, A3, A50, A59, Th3

.= (denaming (V,A,(val . 3))) . Lj by A1, A39, NOMIN_2:10

.= denaming ((val . 3),Lj) by A38, NOMIN_1:def 18

.= Lj . (val . 3) by A37, NOMIN_1:def 12

.= Li . (val . 3) by A1, A2, A4, A34, A36, Th3

.= n0 by A1, A2, A4, A10, A17, A13, A29, Th3 ; :: thesis: ex I, S being Nat st

( I = Ls . (loc /. 1) & S = Ls . (loc /. 4) & S = I ! )

A61: Ln . (val . 4) = Lj . (val . 4) by A1, A2, A4, A42, A39, Th3

.= Li . (val . 4) by A1, A2, A4, A34, A41, Th3

.= 1 by A1, A2, A4, A10, A18, A14, A29, Th3 ;

take 0 ; :: thesis: ex S being Nat st

( 0 = Ls . (loc /. 1) & S = Ls . (loc /. 4) & S = 0 ! )

take 1 ; :: thesis: ( 0 = Ls . (loc /. 1) & 1 = Ls . (loc /. 4) & 1 = 0 ! )

thus Ls . (loc /. 1) = Ln . (loc /. 1) by A1, A2, A3, A50, A54, Th3

.= Lj . (loc /. 1) by A1, A2, A3, A53, A39, Th3

.= Li . (loc /. 1) by A1, A2, A3, A34, A52, Th3

.= (denaming (V,A,(val . 1))) . d1 by A1, A29, NOMIN_2:10

.= denaming ((val . 1),d1) by A28, NOMIN_1:def 18

.= 0 by A10, A11, A15, NOMIN_1:def 12 ; :: thesis: ( 1 = Ls . (loc /. 4) & 1 = 0 ! )

thus Ls . (loc /. 4) = (denaming (V,A,(val . 4))) . Ln by A1, A50, NOMIN_2:10

.= denaming ((val . 4),Ln) by A44, NOMIN_1:def 18

.= 1 by A61, A43, NOMIN_1:def 12 ; :: thesis: 1 = 0 !

thus 1 = 0 ! by NEWTON:12; :: thesis: verum

.= (SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))) . Lj by A47, NOMIN_2:35

.= (SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))) . Ln by A46, NOMIN_2:35

.= (factorial_inv (A,loc,n0)) . Ls by A45, NOMIN_2:35

.= TRUE by A31, A49, Def19 ; :: thesis: verum

A63: <*(PP_inversion (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2)))),(SC_assignment ((denaming (V,A,(val . 2))),(loc /. 2))),(SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3)))*> is SFHT of (ND (V,A)) by NOMIN_4:16;

A64: <*(PP_inversion (SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3)))),(SC_assignment ((denaming (V,A,(val . 3))),(loc /. 3))),(SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4)))*> is SFHT of (ND (V,A)) by NOMIN_4:16;

<*(PP_inversion (SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4)))),(SC_assignment ((denaming (V,A,(val . 4))),(loc /. 4))),(factorial_inv (A,loc,n0))*> is SFHT of (ND (V,A)) by NOMIN_4:16;

hence <*(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 A62, A5, A6, A7, A63, A64, Th2; :: thesis: verum