let V, A be set ; for z being Element of V
for loc being V -valued Function
for n0 being Nat st ( for T being TypeSCNominativeData of V,A holds
( loc /. 1 is_a_value_on T & loc /. 3 is_a_value_on T ) ) holds
<*(PP_inversion (PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))))),(SC_assignment ((denaming (V,A,(loc /. 4))),z)),(valid_factorial_output (A,z,n0))*> is SFHT of (ND (V,A))
let z be Element of V; for loc being V -valued Function
for n0 being Nat st ( for T being TypeSCNominativeData of V,A holds
( loc /. 1 is_a_value_on T & loc /. 3 is_a_value_on T ) ) holds
<*(PP_inversion (PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))))),(SC_assignment ((denaming (V,A,(loc /. 4))),z)),(valid_factorial_output (A,z,n0))*> is SFHT of (ND (V,A))
let loc be V -valued Function; for n0 being Nat st ( for T being TypeSCNominativeData of V,A holds
( loc /. 1 is_a_value_on T & loc /. 3 is_a_value_on T ) ) holds
<*(PP_inversion (PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))))),(SC_assignment ((denaming (V,A,(loc /. 4))),z)),(valid_factorial_output (A,z,n0))*> is SFHT of (ND (V,A))
let n0 be Nat; ( ( for T being TypeSCNominativeData of V,A holds
( loc /. 1 is_a_value_on T & loc /. 3 is_a_value_on T ) ) implies <*(PP_inversion (PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))))),(SC_assignment ((denaming (V,A,(loc /. 4))),z)),(valid_factorial_output (A,z,n0))*> is SFHT of (ND (V,A)) )
set i = loc /. 1;
set j = loc /. 2;
set n = loc /. 3;
set s = loc /. 4;
set D = ND (V,A);
set inv = factorial_inv (A,loc,n0);
set O = valid_factorial_output (A,z,n0);
set Di = denaming (V,A,(loc /. 1));
set Dn = denaming (V,A,(loc /. 3));
set Ds = denaming (V,A,(loc /. 4));
set g = SC_assignment ((denaming (V,A,(loc /. 4))),z);
set E = Equality (A,(loc /. 1),(loc /. 3));
set q = PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0)));
set N = PP_inversion (PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))));
assume A1:
for T being TypeSCNominativeData of V,A holds
( loc /. 1 is_a_value_on T & loc /. 3 is_a_value_on T )
; <*(PP_inversion (PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))))),(SC_assignment ((denaming (V,A,(loc /. 4))),z)),(valid_factorial_output (A,z,n0))*> is SFHT of (ND (V,A))
now for d being TypeSCNominativeData of V,A st d in dom (PP_inversion (PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))))) & (PP_inversion (PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))))) . d = TRUE & d in dom (SC_assignment ((denaming (V,A,(loc /. 4))),z)) & (SC_assignment ((denaming (V,A,(loc /. 4))),z)) . d in dom (valid_factorial_output (A,z,n0)) holds
(valid_factorial_output (A,z,n0)) . ((SC_assignment ((denaming (V,A,(loc /. 4))),z)) . d) = TRUE let d be
TypeSCNominativeData of
V,
A;
( d in dom (PP_inversion (PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))))) & (PP_inversion (PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))))) . d = TRUE & d in dom (SC_assignment ((denaming (V,A,(loc /. 4))),z)) & (SC_assignment ((denaming (V,A,(loc /. 4))),z)) . d in dom (valid_factorial_output (A,z,n0)) implies (valid_factorial_output (A,z,n0)) . ((SC_assignment ((denaming (V,A,(loc /. 4))),z)) . d) = TRUE )assume that A2:
d in dom (PP_inversion (PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0)))))
and
(PP_inversion (PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))))) . d = TRUE
and
d in dom (SC_assignment ((denaming (V,A,(loc /. 4))),z))
and
(SC_assignment ((denaming (V,A,(loc /. 4))),z)) . d in dom (valid_factorial_output (A,z,n0))
;
(valid_factorial_output (A,z,n0)) . ((SC_assignment ((denaming (V,A,(loc /. 4))),z)) . d) = TRUE A3:
dom (PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0)))) = { d where d is Element of ND (V,A) : ( ( d in dom (Equality (A,(loc /. 1),(loc /. 3))) & (Equality (A,(loc /. 1),(loc /. 3))) . d = FALSE ) or ( d in dom (factorial_inv (A,loc,n0)) & (factorial_inv (A,loc,n0)) . d = FALSE ) or ( d in dom (Equality (A,(loc /. 1),(loc /. 3))) & (Equality (A,(loc /. 1),(loc /. 3))) . d = TRUE & d in dom (factorial_inv (A,loc,n0)) & (factorial_inv (A,loc,n0)) . d = TRUE ) ) }
by PARTPR_1:16;
A4:
dom (denaming (V,A,(loc /. 1))) = { d where d is NonatomicND of V,A : loc /. 1 in dom d }
by NOMIN_1:def 18;
A5:
dom (denaming (V,A,(loc /. 3))) = { d where d is NonatomicND of V,A : loc /. 3 in dom d }
by NOMIN_1:def 18;
A6:
dom (Equality (A,(loc /. 1),(loc /. 3))) = (dom (denaming (V,A,(loc /. 1)))) /\ (dom (denaming (V,A,(loc /. 3))))
by A1, NOMIN_4:11;
A7:
not
d in dom (PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))))
by A2, PARTPR_2:9;
dom (Equality (A,(loc /. 1),(loc /. 3))) c= dom (PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))))
by PARTPR_2:3;
then
not
d in dom (Equality (A,(loc /. 1),(loc /. 3)))
by A2, PARTPR_2:9;
then A8:
( not
d in dom (denaming (V,A,(loc /. 1))) or not
d in dom (denaming (V,A,(loc /. 3))) )
by A6, XBOOLE_0:def 4;
dom (factorial_inv (A,loc,n0)) = ND (
V,
A)
by Def19;
then A9:
d in dom (factorial_inv (A,loc,n0))
;
then
(factorial_inv (A,loc,n0)) . d <> FALSE
by A3, A7;
then
factorial_inv_pred A,
loc,
n0,
d
by A9, Def19;
then consider d1 being
NonatomicND of
V,
A such that A10:
d = d1
and A11:
{(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4)} c= dom d1
and
(
d1 . (loc /. 2) = 1 &
d1 . (loc /. 3) = n0 & ex
I,
S being
Nat st
(
I = d1 . (loc /. 1) &
S = d1 . (loc /. 4) &
S = I ! ) )
;
(
loc /. 1
in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4)} &
loc /. 3
in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4)} )
by ENUMSET1:def 2;
hence
(valid_factorial_output (A,z,n0)) . ((SC_assignment ((denaming (V,A,(loc /. 4))),z)) . d) = TRUE
by A4, A5, A8, A10, A11;
verum end;
hence
<*(PP_inversion (PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))))),(SC_assignment ((denaming (V,A,(loc /. 4))),z)),(valid_factorial_output (A,z,n0))*> is SFHT of (ND (V,A))
by NOMIN_3:28; verum