let V, A be set ; 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; 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; ( 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
; <*(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 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 let d be
TypeSCNominativeData of
V,
A;
( 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))
;
(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
take
Lm
;
NOMIN_5:def 18 ( 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
;
( {(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;
( 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
;
( 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
;
ex I, S being Nat st
( I = Lm . (loc /. 1) & S = Lm . (loc /. 4) & S = I ! )
take I1 =
I + 1;
ex S being Nat st
( I1 = Lm . (loc /. 1) & S = Lm . (loc /. 4) & S = I1 ! )
take S1 =
S * (I + 1);
( 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;
( 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
;
S1 = I1 !
thus
S1 = I1 !
by A20, NEWTON:15;
verum
end; hence
(factorial_inv (A,loc,n0)) . ((factorial_loop_body (A,loc)) . d) = TRUE
by A8, A25, A26, A28, Def19;
verum 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; verum