let V, A be set ; 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; 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; 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; ( 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 )
; 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); NOMIN_3:def 3 ( 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
; ( 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; (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
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
;
NOMIN_5:def 16 ( 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
;
( z in dom dlo & dlo . z = n0 ! )
thus
z in dom dlo
by A28;
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;
verum
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
;
verum