let V, A be set ; :: thesis:
let loc be V -valued Function; :: thesis:
let n0 be Nat; :: thesis:
set i = loc /. 1;
set j = loc /. 2;
set n = loc /. 3;
set s = loc /. 4;
assume that
A1: not V is empty and
A2: A is complex-containing and
A3: A is_without_nonatomicND_wrt V and
A4: loc /. 1,loc /. 2,loc /. 3,loc /. 4 are_mutually_distinct ; :: thesis:
set D = ND (V,A);
set inv = factorial_inv (A,loc,n0);
set B = factorial_loop_body (A,loc);
set add = addition (A,(loc /. 1),(loc /. 2));
set mlt = multiplication (A,(loc /. 4),(loc /. 1));
set f = SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1));
set g = SC_assignment ((multiplication (A,(loc /. 4),(loc /. 1))),(loc /. 4));
set Di = denaming (V,A,(loc /. 1));
set Dj = denaming (V,A,(loc /. 2));
set Dn = denaming (V,A,(loc /. 3));
set Ds = denaming (V,A,(loc /. 4));

now :: thesis:

let d be TypeSCNominativeData of V,A; :: thesis:
assume that
A5: d in dom (factorial_inv (A,loc,n0)) and
A6: (factorial_inv (A,loc,n0)) . d = TRUE and
A7: d in dom (factorial_loop_body (A,loc)) and
A8: (factorial_loop_body (A,loc)) . d in dom (factorial_inv (A,loc,n0)) ; :: thesis:
factorial_inv_pred A,loc,n0,d by A5, A6, Def19;
then consider d1 being NonatomicND of V,A such that
A9: d = d1 and
A10: {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4)} c= dom d1 and
A11: d1 . (loc /. 2) = 1 and
A12: d1 . (loc /. 3) = n0 and
A13: ex I, S being Nat st
( I = d1 . (loc /. 1) & S = d1 . (loc /. 4) & S = I ! ) ;
A14: loc /. 1 in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4)} by ENUMSET1:def 2;
A15: loc /. 2 in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4)} by ENUMSET1:def 2;
A16: loc /. 3 in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4)} by ENUMSET1:def 2;
A17: loc /. 4 in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4)} by ENUMSET1:def 2;
consider I, S being Nat such that
A18: I = d1 . (loc /. 1) and
A19: S = d1 . (loc /. 4) and
A20: S = I ! by A13;
A21: dom (SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) = dom (addition (A,(loc /. 1),(loc /. 2))) by NOMIN_2:def 7;
A22: dom (SC_assignment ((multiplication (A,(loc /. 4),(loc /. 1))),(loc /. 4))) = dom (multiplication (A,(loc /. 4),(loc /. 1))) by NOMIN_2:def 7;
A23: PP_composition ((SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))),(SC_assignment ((multiplication (A,(loc /. 4),(loc /. 1))),(loc /. 4)))) = (SC_assignment ((multiplication (A,(loc /. 4),(loc /. 1))),(loc /. 4))) * (SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) by PARTPR_2:def 1;
then A24: d in dom (SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) by A7, FUNCT_1:11;
then reconsider Ad = (addition (A,(loc /. 1),(loc /. 2))) . d1 as TypeSCNominativeData of V,A by A21, A9, PARTFUN1:4, NOMIN_1:39;
reconsider La = local_overlapping (V,A,d1,Ad,(loc /. 1)) as NonatomicND of V,A by NOMIN_2:9;
reconsider Lm = local_overlapping (V,A,La,((multiplication (A,(loc /. 4),(loc /. 1))) . La),(loc /. 4)) as NonatomicND of V,A by NOMIN_2:9;
factorial_loop_body (A,loc) = (SC_assignment ((multiplication (A,(loc /. 4),(loc /. 1))),(loc /. 4))) * (SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) by PARTPR_2:def 1;
then A25: (factorial_loop_body (A,loc)) . d = (SC_assignment ((multiplication (A,(loc /. 4),(loc /. 1))),(loc /. 4))) . ((SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) . d) by A7, FUNCT_1:12;
A26: (SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) . d = La by A9, A24, NOMIN_2:def 7;
then A27: La in dom (SC_assignment ((multiplication (A,(loc /. 4),(loc /. 1))),(loc /. 4))) by A7, A23, FUNCT_1:11;
A28: (SC_assignment ((multiplication (A,(loc /. 4),(loc /. 1))),(loc /. 4))) . La = Lm by A27, NOMIN_2:def 7;
factorial_inv_pred A,loc,n0,Lm

proof

take Lm ; :: according to NOMIN_5:def 18 :: thesis:
thus Lm = Lm ; :: thesis:
A29: (multiplication (A,(loc /. 4),(loc /. 1))) . La is TypeSCNominativeData of V,A by A22, A27, PARTFUN1:4, NOMIN_1:39;
A30: dom Lm = (dom La) \/ {(loc /. 4)} by A3, A1, A22, A27, A28, NOMIN_4:5;
A31: dom La = {(loc /. 1)} \/ (dom d1) by A3, A1, NOMIN_4:4;
loc /. 1 in {(loc /. 1)} by TARSKI:def 1;
then A32: loc /. 1 in dom La by A31, XBOOLE_0:def 3;
then A33: loc /. 1 in dom Lm by A30, XBOOLE_0:def 3;
A34: loc /. 2 in dom La by A10, A15, A31, XBOOLE_0:def 3;
then A35: loc /. 2 in dom Lm by A30, XBOOLE_0:def 3;
A36: loc /. 3 in dom La by A10, A16, A31, XBOOLE_0:def 3;
then A37: loc /. 3 in dom Lm by A30, XBOOLE_0:def 3;
loc /. 4 in {(loc /. 4)} by TARSKI:def 1;
then loc /. 4 in dom Lm by A30, XBOOLE_0:def 3;
hence {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4)} c= dom Lm by A33, A35, A37, ENUMSET1:def 2; :: thesis:
thus Lm . (loc /. 2) = La . (loc /. 2) by A1, A3, A4, A29, A34, Th3
.= 1 by A3, A1, A10, A15, A11, A4, Th3 ; :: thesis:
thus Lm . (loc /. 3) = La . (loc /. 3) by A4, A1, A29, A36, A3, Th3
.= n0 by A3, A1, A4, A10, A16, A12, Th3 ; :: thesis:
take I1 = I + 1; :: thesis:
take S1 = S * (I + 1); :: thesis:
A38: La . (loc /. 1) = Ad by A1, NOMIN_2:10
.= I1 by A14, A2, A18, A10, A11, A15, A9, A24, A21, Th4 ;
hence Lm . (loc /. 1) = I1 by A1, A29, A3, A4, A32, Th3; :: thesis:
A39: loc /. 4 in dom La by A10, A17, A31, XBOOLE_0:def 3;
A40: La . (loc /. 4) = d1 . (loc /. 4) by A3, A1, A10, A4, A17, Th3;
thus Lm . (loc /. 4) = (multiplication (A,(loc /. 4),(loc /. 1))) . La by A1, A29, NOMIN_2:10
.= S1 by A32, A2, A19, A39, A22, A27, A38, A40, Th5 ; :: thesis:
thus S1 = I1 ! by A20, NEWTON:15; :: thesis:

end;

hence (factorial_inv (A,loc,n0)) . ((factorial_loop_body (A,loc)) . d) = TRUE by A8, A25, A26, A28, Def19; :: thesis:

end;

hence <*(factorial_inv (A,loc,n0)),(factorial_loop_body (A,loc)),(factorial_inv (A,loc,n0))*> is SFHT of (ND (V,A)) by NOMIN_3:28; :: thesis: