let V, A be set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( ( 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 ) ; :: thesis: <*(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))

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; :: thesis: 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; :: thesis: 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; :: thesis: ( ( 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 ) ; :: thesis: <*(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 :: thesis: 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

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; :: thesis: verum(valid_factorial_output (A,z,n0)) . ((SC_assignment ((denaming (V,A,(loc /. 4))),z)) . d) = TRUE

let d be TypeSCNominativeData of V,A; :: thesis: ( 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)) ; :: thesis: (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; :: thesis: verum

end;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)) ; :: thesis: (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; :: thesis: verum