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_loop_body (A,loc)),(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_loop_body (A,loc)),(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_loop_body (A,loc)),(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;

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

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));

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_loop_body (A,loc)),(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_loop_body (A,loc)),(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_loop_body (A,loc)),(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;

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

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: for d being TypeSCNominativeData of V,A st d in dom (factorial_inv (A,loc,n0)) & (factorial_inv (A,loc,n0)) . d = TRUE & d in dom (factorial_loop_body (A,loc)) & (factorial_loop_body (A,loc)) . d in dom (factorial_inv (A,loc,n0)) holds

(factorial_inv (A,loc,n0)) . ((factorial_loop_body (A,loc)) . d) = TRUE

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: verum(factorial_inv (A,loc,n0)) . ((factorial_loop_body (A,loc)) . d) = TRUE

let d be TypeSCNominativeData of V,A; :: thesis: ( d in dom (factorial_inv (A,loc,n0)) & (factorial_inv (A,loc,n0)) . d = TRUE & d in dom (factorial_loop_body (A,loc)) & (factorial_loop_body (A,loc)) . d in dom (factorial_inv (A,loc,n0)) implies (factorial_inv (A,loc,n0)) . ((factorial_loop_body (A,loc)) . d) = TRUE )

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 (A,loc,n0)) . ((factorial_loop_body (A,loc)) . d) = TRUE

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

end;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 (A,loc,n0)) . ((factorial_loop_body (A,loc)) . d) = TRUE

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

hence
(factorial_inv (A,loc,n0)) . ((factorial_loop_body (A,loc)) . d) = TRUE
by A8, A25, A26, A28, Def19; :: thesis: verum
take
Lm
; :: according to NOMIN_5:def 18 :: thesis: ( Lm = Lm & {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4)} c= dom Lm & Lm . (loc /. 2) = 1 & Lm . (loc /. 3) = n0 & ex I, S being Nat st

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

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

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

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: ( Lm . (loc /. 2) = 1 & Lm . (loc /. 3) = n0 & ex I, S being Nat st

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

thus Lm . (loc /. 2) = La . (loc /. 2) by A1, A3, A4, A29, A34, Th3

.= 1 by A3, A1, A10, A15, A11, A4, Th3 ; :: thesis: ( Lm . (loc /. 3) = n0 & ex I, S being Nat st

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

thus Lm . (loc /. 3) = La . (loc /. 3) by A4, A1, A29, A36, A3, Th3

.= n0 by A3, A1, A4, A10, A16, A12, Th3 ; :: thesis: ex I, S being Nat st

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

take I1 = I + 1; :: thesis: ex S being Nat st

( I1 = Lm . (loc /. 1) & S = Lm . (loc /. 4) & S = I1 ! )

take S1 = S * (I + 1); :: thesis: ( I1 = Lm . (loc /. 1) & S1 = Lm . (loc /. 4) & S1 = I1 ! )

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: ( S1 = Lm . (loc /. 4) & S1 = I1 ! )

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: S1 = I1 !

thus S1 = I1 ! by A20, NEWTON:15; :: thesis: verum

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

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

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

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: ( Lm . (loc /. 2) = 1 & Lm . (loc /. 3) = n0 & ex I, S being Nat st

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

thus Lm . (loc /. 2) = La . (loc /. 2) by A1, A3, A4, A29, A34, Th3

.= 1 by A3, A1, A10, A15, A11, A4, Th3 ; :: thesis: ( Lm . (loc /. 3) = n0 & ex I, S being Nat st

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

thus Lm . (loc /. 3) = La . (loc /. 3) by A4, A1, A29, A36, A3, Th3

.= n0 by A3, A1, A4, A10, A16, A12, Th3 ; :: thesis: ex I, S being Nat st

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

take I1 = I + 1; :: thesis: ex S being Nat st

( I1 = Lm . (loc /. 1) & S = Lm . (loc /. 4) & S = I1 ! )

take S1 = S * (I + 1); :: thesis: ( I1 = Lm . (loc /. 1) & S1 = Lm . (loc /. 4) & S1 = I1 ! )

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: ( S1 = Lm . (loc /. 4) & S1 = I1 ! )

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: S1 = I1 !

thus S1 = I1 ! by A20, NEWTON:15; :: thesis: verum