let V, A be set ; :: thesis: for z being Element of V

for loc being V -valued Function

for n0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & ( for T being TypeSCNominativeData of V,A holds

( loc /. 1 is_a_value_on T & loc /. 3 is_a_value_on T ) ) holds

PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))) ||= SC_Psuperpos ((valid_factorial_output (A,z,n0)),(denaming (V,A,(loc /. 4))),z)

let z be Element of V; :: thesis: for loc being V -valued Function

for n0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & ( for T being TypeSCNominativeData of V,A holds

( loc /. 1 is_a_value_on T & loc /. 3 is_a_value_on T ) ) holds

PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))) ||= SC_Psuperpos ((valid_factorial_output (A,z,n0)),(denaming (V,A,(loc /. 4))),z)

let loc be V -valued Function; :: thesis: for n0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & ( for T being TypeSCNominativeData of V,A holds

( loc /. 1 is_a_value_on T & loc /. 3 is_a_value_on T ) ) holds

PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))) ||= SC_Psuperpos ((valid_factorial_output (A,z,n0)),(denaming (V,A,(loc /. 4))),z)

let n0 be Nat; :: thesis: ( not V is empty & A is_without_nonatomicND_wrt V & ( for T being TypeSCNominativeData of V,A holds

( loc /. 1 is_a_value_on T & loc /. 3 is_a_value_on T ) ) implies PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))) ||= SC_Psuperpos ((valid_factorial_output (A,z,n0)),(denaming (V,A,(loc /. 4))),z) )

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 Di = denaming (V,A,(loc /. 1));

set Dn = denaming (V,A,(loc /. 3));

set Ds = denaming (V,A,(loc /. 4));

set Dz = denaming (V,A,z);

set ass = SC_assignment ((denaming (V,A,(loc /. 4))),z);

set out = valid_factorial_output (A,z,n0);

set p = SC_Psuperpos ((valid_factorial_output (A,z,n0)),(denaming (V,A,(loc /. 4))),z);

set E = Equality (A,(loc /. 1),(loc /. 3));

assume that

A1: ( not V is empty & A is_without_nonatomicND_wrt V ) and

A2: for T being TypeSCNominativeData of V,A holds

( loc /. 1 is_a_value_on T & loc /. 3 is_a_value_on T ) ; :: thesis: PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))) ||= SC_Psuperpos ((valid_factorial_output (A,z,n0)),(denaming (V,A,(loc /. 4))),z)

let d be Element of ND (V,A); :: according to NOMIN_3:def 3 :: thesis: ( not d in dom (PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0)))) or not (PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0)))) . d = TRUE or ( d in dom (SC_Psuperpos ((valid_factorial_output (A,z,n0)),(denaming (V,A,(loc /. 4))),z)) & (SC_Psuperpos ((valid_factorial_output (A,z,n0)),(denaming (V,A,(loc /. 4))),z)) . d = TRUE ) )

assume that

A3: d in dom (PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0)))) and

A4: (PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0)))) . d = TRUE ; :: thesis: ( d in dom (SC_Psuperpos ((valid_factorial_output (A,z,n0)),(denaming (V,A,(loc /. 4))),z)) & (SC_Psuperpos ((valid_factorial_output (A,z,n0)),(denaming (V,A,(loc /. 4))),z)) . d = TRUE )

A5: dom (SC_Psuperpos ((valid_factorial_output (A,z,n0)),(denaming (V,A,(loc /. 4))),z)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,(loc /. 4))) . d),z) in dom (valid_factorial_output (A,z,n0)) & d in dom (denaming (V,A,(loc /. 4))) ) } by NOMIN_2:def 11;

A6: dom (valid_factorial_output (A,z,n0)) = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } by Def17;

A7: dom (denaming (V,A,(loc /. 4))) = { d where d is NonatomicND of V,A : loc /. 4 in dom d } by NOMIN_1:def 18;

A8: dom (denaming (V,A,z)) = { d where d is NonatomicND of V,A : z in dom d } by NOMIN_1:def 18;

A9: d in dom (Equality (A,(loc /. 1),(loc /. 3))) by A3, A4, PARTPR_1:23;

A10: d in dom (factorial_inv (A,loc,n0)) by A3, A4, PARTPR_1:23;

A11: dom (Equality (A,(loc /. 1),(loc /. 3))) = (dom (denaming (V,A,(loc /. 1)))) /\ (dom (denaming (V,A,(loc /. 3)))) by A2, NOMIN_4:11;

then A12: d in dom (denaming (V,A,(loc /. 1))) by A9, XBOOLE_0:def 4;

(factorial_inv (A,loc,n0)) . d = TRUE by A3, A4, PARTPR_1:23;

then factorial_inv_pred A,loc,n0,d by A10, Def19;

then consider d1 being NonatomicND of V,A such that

A13: d = d1 and

A14: {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4)} c= dom d1 and

d1 . (loc /. 2) = 1 and

A15: d1 . (loc /. 3) = n0 and

A16: ex I, S being Nat st

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

A17: loc /. 1 in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4)} by ENUMSET1:def 2;

A18: loc /. 3 in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4)} by ENUMSET1:def 2;

A19: loc /. 4 in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4)} by ENUMSET1:def 2;

reconsider dd = d as TypeSCNominativeData of V,A by NOMIN_1:39;

set L = local_overlapping (V,A,dd,((denaming (V,A,(loc /. 4))) . dd),z);

A20: dd in dom (denaming (V,A,(loc /. 4))) by A7, A13, A14, A19;

then (denaming (V,A,(loc /. 4))) . d1 in ND (V,A) by A13, PARTFUN1:4;

then A21: ex d2 being TypeSCNominativeData of V,A st (denaming (V,A,(loc /. 4))) . d1 = d2 ;

then A22: local_overlapping (V,A,dd,((denaming (V,A,(loc /. 4))) . dd),z) in dom (denaming (V,A,z)) by A1, A13, NOMIN_4:6;

then A23: local_overlapping (V,A,dd,((denaming (V,A,(loc /. 4))) . dd),z) in dom (valid_factorial_output (A,z,n0)) by A6;

hence A24: d in dom (SC_Psuperpos ((valid_factorial_output (A,z,n0)),(denaming (V,A,(loc /. 4))),z)) by A5, A20; :: thesis: (SC_Psuperpos ((valid_factorial_output (A,z,n0)),(denaming (V,A,(loc /. 4))),z)) . d = TRUE

valid_factorial_output_pred A,z,n0, local_overlapping (V,A,dd,((denaming (V,A,(loc /. 4))) . dd),z)

.= (SC_Psuperpos ((valid_factorial_output (A,z,n0)),(denaming (V,A,(loc /. 4))),z)) . d by A24, NOMIN_2:35 ;

:: thesis: verum

for loc being V -valued Function

for n0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & ( for T being TypeSCNominativeData of V,A holds

( loc /. 1 is_a_value_on T & loc /. 3 is_a_value_on T ) ) holds

PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))) ||= SC_Psuperpos ((valid_factorial_output (A,z,n0)),(denaming (V,A,(loc /. 4))),z)

let z be Element of V; :: thesis: for loc being V -valued Function

for n0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & ( for T being TypeSCNominativeData of V,A holds

( loc /. 1 is_a_value_on T & loc /. 3 is_a_value_on T ) ) holds

PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))) ||= SC_Psuperpos ((valid_factorial_output (A,z,n0)),(denaming (V,A,(loc /. 4))),z)

let loc be V -valued Function; :: thesis: for n0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & ( for T being TypeSCNominativeData of V,A holds

( loc /. 1 is_a_value_on T & loc /. 3 is_a_value_on T ) ) holds

PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))) ||= SC_Psuperpos ((valid_factorial_output (A,z,n0)),(denaming (V,A,(loc /. 4))),z)

let n0 be Nat; :: thesis: ( not V is empty & A is_without_nonatomicND_wrt V & ( for T being TypeSCNominativeData of V,A holds

( loc /. 1 is_a_value_on T & loc /. 3 is_a_value_on T ) ) implies PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))) ||= SC_Psuperpos ((valid_factorial_output (A,z,n0)),(denaming (V,A,(loc /. 4))),z) )

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 Di = denaming (V,A,(loc /. 1));

set Dn = denaming (V,A,(loc /. 3));

set Ds = denaming (V,A,(loc /. 4));

set Dz = denaming (V,A,z);

set ass = SC_assignment ((denaming (V,A,(loc /. 4))),z);

set out = valid_factorial_output (A,z,n0);

set p = SC_Psuperpos ((valid_factorial_output (A,z,n0)),(denaming (V,A,(loc /. 4))),z);

set E = Equality (A,(loc /. 1),(loc /. 3));

assume that

A1: ( not V is empty & A is_without_nonatomicND_wrt V ) and

A2: for T being TypeSCNominativeData of V,A holds

( loc /. 1 is_a_value_on T & loc /. 3 is_a_value_on T ) ; :: thesis: PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0))) ||= SC_Psuperpos ((valid_factorial_output (A,z,n0)),(denaming (V,A,(loc /. 4))),z)

let d be Element of ND (V,A); :: according to NOMIN_3:def 3 :: thesis: ( not d in dom (PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0)))) or not (PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0)))) . d = TRUE or ( d in dom (SC_Psuperpos ((valid_factorial_output (A,z,n0)),(denaming (V,A,(loc /. 4))),z)) & (SC_Psuperpos ((valid_factorial_output (A,z,n0)),(denaming (V,A,(loc /. 4))),z)) . d = TRUE ) )

assume that

A3: d in dom (PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0)))) and

A4: (PP_and ((Equality (A,(loc /. 1),(loc /. 3))),(factorial_inv (A,loc,n0)))) . d = TRUE ; :: thesis: ( d in dom (SC_Psuperpos ((valid_factorial_output (A,z,n0)),(denaming (V,A,(loc /. 4))),z)) & (SC_Psuperpos ((valid_factorial_output (A,z,n0)),(denaming (V,A,(loc /. 4))),z)) . d = TRUE )

A5: dom (SC_Psuperpos ((valid_factorial_output (A,z,n0)),(denaming (V,A,(loc /. 4))),z)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,(loc /. 4))) . d),z) in dom (valid_factorial_output (A,z,n0)) & d in dom (denaming (V,A,(loc /. 4))) ) } by NOMIN_2:def 11;

A6: dom (valid_factorial_output (A,z,n0)) = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } by Def17;

A7: dom (denaming (V,A,(loc /. 4))) = { d where d is NonatomicND of V,A : loc /. 4 in dom d } by NOMIN_1:def 18;

A8: dom (denaming (V,A,z)) = { d where d is NonatomicND of V,A : z in dom d } by NOMIN_1:def 18;

A9: d in dom (Equality (A,(loc /. 1),(loc /. 3))) by A3, A4, PARTPR_1:23;

A10: d in dom (factorial_inv (A,loc,n0)) by A3, A4, PARTPR_1:23;

A11: dom (Equality (A,(loc /. 1),(loc /. 3))) = (dom (denaming (V,A,(loc /. 1)))) /\ (dom (denaming (V,A,(loc /. 3)))) by A2, NOMIN_4:11;

then A12: d in dom (denaming (V,A,(loc /. 1))) by A9, XBOOLE_0:def 4;

(factorial_inv (A,loc,n0)) . d = TRUE by A3, A4, PARTPR_1:23;

then factorial_inv_pred A,loc,n0,d by A10, Def19;

then consider d1 being NonatomicND of V,A such that

A13: d = d1 and

A14: {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4)} c= dom d1 and

d1 . (loc /. 2) = 1 and

A15: d1 . (loc /. 3) = n0 and

A16: ex I, S being Nat st

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

A17: loc /. 1 in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4)} by ENUMSET1:def 2;

A18: loc /. 3 in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4)} by ENUMSET1:def 2;

A19: loc /. 4 in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4)} by ENUMSET1:def 2;

reconsider dd = d as TypeSCNominativeData of V,A by NOMIN_1:39;

set L = local_overlapping (V,A,dd,((denaming (V,A,(loc /. 4))) . dd),z);

A20: dd in dom (denaming (V,A,(loc /. 4))) by A7, A13, A14, A19;

then (denaming (V,A,(loc /. 4))) . d1 in ND (V,A) by A13, PARTFUN1:4;

then A21: ex d2 being TypeSCNominativeData of V,A st (denaming (V,A,(loc /. 4))) . d1 = d2 ;

then A22: local_overlapping (V,A,dd,((denaming (V,A,(loc /. 4))) . dd),z) in dom (denaming (V,A,z)) by A1, A13, NOMIN_4:6;

then A23: local_overlapping (V,A,dd,((denaming (V,A,(loc /. 4))) . dd),z) in dom (valid_factorial_output (A,z,n0)) by A6;

hence A24: d in dom (SC_Psuperpos ((valid_factorial_output (A,z,n0)),(denaming (V,A,(loc /. 4))),z)) by A5, A20; :: thesis: (SC_Psuperpos ((valid_factorial_output (A,z,n0)),(denaming (V,A,(loc /. 4))),z)) . d = TRUE

valid_factorial_output_pred A,z,n0, local_overlapping (V,A,dd,((denaming (V,A,(loc /. 4))) . dd),z)

proof

hence TRUE =
(valid_factorial_output (A,z,n0)) . (local_overlapping (V,A,dd,((denaming (V,A,(loc /. 4))) . dd),z))
by A23, Def17
consider I, S being Nat such that

A25: I = d1 . (loc /. 1) and

A26: S = d1 . (loc /. 4) and

A27: S = I ! by A16;

A28: ex d being NonatomicND of V,A st

( local_overlapping (V,A,dd,((denaming (V,A,(loc /. 4))) . dd),z) = d & z in dom d ) by A8, A22;

then reconsider dlo = local_overlapping (V,A,dd,((denaming (V,A,(loc /. 4))) . dd),z) as NonatomicND of V,A ;

take dlo ; :: according to NOMIN_5:def 16 :: thesis: ( local_overlapping (V,A,dd,((denaming (V,A,(loc /. 4))) . dd),z) = dlo & z in dom dlo & dlo . z = n0 ! )

thus local_overlapping (V,A,dd,((denaming (V,A,(loc /. 4))) . dd),z) = dlo ; :: thesis: ( z in dom dlo & dlo . z = n0 ! )

thus z in dom dlo by A28; :: thesis: dlo . z = n0 !

A29: loc /. 1 is_a_value_on dd by A2;

A30: loc /. 3 is_a_value_on dd by A2;

A31: dom <:(denaming (V,A,(loc /. 1))),(denaming (V,A,(loc /. 3))):> = (dom (denaming (V,A,(loc /. 1)))) /\ (dom (denaming (V,A,(loc /. 3)))) by FUNCT_3:def 7;

d in dom <:(denaming (V,A,(loc /. 1))),(denaming (V,A,(loc /. 3))):> by A9, A11, FUNCT_3:def 7;

then A32: (Equality (A,(loc /. 1),(loc /. 3))) . d = (Equality A) . (<:(denaming (V,A,(loc /. 1))),(denaming (V,A,(loc /. 3))):> . d) by FUNCT_1:13;

A33: d in dom (denaming (V,A,(loc /. 3))) by A9, A11, XBOOLE_0:def 4;

A34: <:(denaming (V,A,(loc /. 1))),(denaming (V,A,(loc /. 3))):> . d = [((denaming (V,A,(loc /. 1))) . d),((denaming (V,A,(loc /. 3))) . d)] by A9, A11, A31, FUNCT_3:def 7;

A35: (denaming (V,A,(loc /. 1))) . d = denaming ((loc /. 1),d1) by A13, A12, NOMIN_1:def 18

.= d1 . (loc /. 1) by A14, A17, NOMIN_1:def 12 ;

A36: (denaming (V,A,(loc /. 3))) . d = denaming ((loc /. 3),d1) by A13, A33, NOMIN_1:def 18

.= d1 . (loc /. 3) by A14, A18, NOMIN_1:def 12 ;

A37: (denaming (V,A,(loc /. 4))) . d = denaming ((loc /. 4),d1) by A20, A13, NOMIN_1:def 18

.= d1 . (loc /. 4) by A14, A19, NOMIN_1:def 12 ;

(Equality A) . (((denaming (V,A,(loc /. 1))) . d),((denaming (V,A,(loc /. 3))) . d)) <> FALSE by A3, A4, A32, A34, PARTPR_1:23;

then (denaming (V,A,(loc /. 1))) . d = (denaming (V,A,(loc /. 3))) . d by A29, A30, NOMIN_4:def 9;

hence dlo . z = n0 ! by A1, A13, A15, A21, A25, A26, A27, A35, A36, A37, NOMIN_2:10; :: thesis: verum

end;A25: I = d1 . (loc /. 1) and

A26: S = d1 . (loc /. 4) and

A27: S = I ! by A16;

A28: ex d being NonatomicND of V,A st

( local_overlapping (V,A,dd,((denaming (V,A,(loc /. 4))) . dd),z) = d & z in dom d ) by A8, A22;

then reconsider dlo = local_overlapping (V,A,dd,((denaming (V,A,(loc /. 4))) . dd),z) as NonatomicND of V,A ;

take dlo ; :: according to NOMIN_5:def 16 :: thesis: ( local_overlapping (V,A,dd,((denaming (V,A,(loc /. 4))) . dd),z) = dlo & z in dom dlo & dlo . z = n0 ! )

thus local_overlapping (V,A,dd,((denaming (V,A,(loc /. 4))) . dd),z) = dlo ; :: thesis: ( z in dom dlo & dlo . z = n0 ! )

thus z in dom dlo by A28; :: thesis: dlo . z = n0 !

A29: loc /. 1 is_a_value_on dd by A2;

A30: loc /. 3 is_a_value_on dd by A2;

A31: dom <:(denaming (V,A,(loc /. 1))),(denaming (V,A,(loc /. 3))):> = (dom (denaming (V,A,(loc /. 1)))) /\ (dom (denaming (V,A,(loc /. 3)))) by FUNCT_3:def 7;

d in dom <:(denaming (V,A,(loc /. 1))),(denaming (V,A,(loc /. 3))):> by A9, A11, FUNCT_3:def 7;

then A32: (Equality (A,(loc /. 1),(loc /. 3))) . d = (Equality A) . (<:(denaming (V,A,(loc /. 1))),(denaming (V,A,(loc /. 3))):> . d) by FUNCT_1:13;

A33: d in dom (denaming (V,A,(loc /. 3))) by A9, A11, XBOOLE_0:def 4;

A34: <:(denaming (V,A,(loc /. 1))),(denaming (V,A,(loc /. 3))):> . d = [((denaming (V,A,(loc /. 1))) . d),((denaming (V,A,(loc /. 3))) . d)] by A9, A11, A31, FUNCT_3:def 7;

A35: (denaming (V,A,(loc /. 1))) . d = denaming ((loc /. 1),d1) by A13, A12, NOMIN_1:def 18

.= d1 . (loc /. 1) by A14, A17, NOMIN_1:def 12 ;

A36: (denaming (V,A,(loc /. 3))) . d = denaming ((loc /. 3),d1) by A13, A33, NOMIN_1:def 18

.= d1 . (loc /. 3) by A14, A18, NOMIN_1:def 12 ;

A37: (denaming (V,A,(loc /. 4))) . d = denaming ((loc /. 4),d1) by A20, A13, NOMIN_1:def 18

.= d1 . (loc /. 4) by A14, A19, NOMIN_1:def 12 ;

(Equality A) . (((denaming (V,A,(loc /. 1))) . d),((denaming (V,A,(loc /. 3))) . d)) <> FALSE by A3, A4, A32, A34, PARTPR_1:23;

then (denaming (V,A,(loc /. 1))) . d = (denaming (V,A,(loc /. 3))) . d by A29, A30, NOMIN_4:def 9;

hence dlo . z = n0 ! by A1, A13, A15, A21, A25, A26, A27, A35, A36, A37, NOMIN_2:10; :: thesis: verum

.= (SC_Psuperpos ((valid_factorial_output (A,z,n0)),(denaming (V,A,(loc /. 4))),z)) . d by A24, NOMIN_2:35 ;

:: thesis: verum