let V, A be set ; :: thesis:
let z be Element of V; :: thesis:
let loc be V -valued Function; :: thesis:
let n0 be Nat; :: thesis:
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:
let d be Element of ND (V,A); :: according to NOMIN_3:def 3 :: thesis:
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:
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:
valid_factorial_output_pred A,z,n0, local_overlapping (V,A,dd,((denaming (V,A,(loc /. 4))) . dd),z)

proof

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:
thus local_overlapping (V,A,dd,((denaming (V,A,(loc /. 4))) . dd),z) = dlo ; :: thesis:
thus z in dom dlo by A28; :: thesis:
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:

end;

hence TRUE = (valid_factorial_output (A,z,n0)) . (local_overlapping (V,A,dd,((denaming (V,A,(loc /. 4))) . dd),z)) by A23, Def17
.= (SC_Psuperpos ((valid_factorial_output (A,z,n0)),(denaming (V,A,(loc /. 4))),z)) . d by A24, NOMIN_2:35 ;
:: thesis: