let V, A be set ; for loc being V -valued Function
for val being Function
for n0 being Nat
for b0 being Complex st not V is empty & A is_without_nonatomicND_wrt V & loc /. 1,loc /. 2,loc /. 3,loc /. 4,loc /. 5 are_mutually_distinct & loc,val are_compatible_wrt_5_locs holds
<*(valid_power_input (V,A,val,b0,n0)),(power_var_init (A,loc,val)),(power_inv (A,loc,b0,n0))*> is SFHT of (ND (V,A))
let loc be V -valued Function; for val being Function
for n0 being Nat
for b0 being Complex st not V is empty & A is_without_nonatomicND_wrt V & loc /. 1,loc /. 2,loc /. 3,loc /. 4,loc /. 5 are_mutually_distinct & loc,val are_compatible_wrt_5_locs holds
<*(valid_power_input (V,A,val,b0,n0)),(power_var_init (A,loc,val)),(power_inv (A,loc,b0,n0))*> is SFHT of (ND (V,A))
let val be Function; for n0 being Nat
for b0 being Complex st not V is empty & A is_without_nonatomicND_wrt V & loc /. 1,loc /. 2,loc /. 3,loc /. 4,loc /. 5 are_mutually_distinct & loc,val are_compatible_wrt_5_locs holds
<*(valid_power_input (V,A,val,b0,n0)),(power_var_init (A,loc,val)),(power_inv (A,loc,b0,n0))*> is SFHT of (ND (V,A))
let n0 be Nat; for b0 being Complex st not V is empty & A is_without_nonatomicND_wrt V & loc /. 1,loc /. 2,loc /. 3,loc /. 4,loc /. 5 are_mutually_distinct & loc,val are_compatible_wrt_5_locs holds
<*(valid_power_input (V,A,val,b0,n0)),(power_var_init (A,loc,val)),(power_inv (A,loc,b0,n0))*> is SFHT of (ND (V,A))
let b0 be Complex; ( not V is empty & A is_without_nonatomicND_wrt V & loc /. 1,loc /. 2,loc /. 3,loc /. 4,loc /. 5 are_mutually_distinct & loc,val are_compatible_wrt_5_locs implies <*(valid_power_input (V,A,val,b0,n0)),(power_var_init (A,loc,val)),(power_inv (A,loc,b0,n0))*> is SFHT of (ND (V,A)) )
set i = loc /. 1;
set j = loc /. 2;
set b = loc /. 3;
set n = loc /. 4;
set s = loc /. 5;
set i1 = val . 1;
set j1 = val . 2;
set b1 = val . 3;
set n1 = val . 4;
set s1 = val . 5;
set D = ND (V,A);
set I = valid_power_input (V,A,val,b0,n0);
set F = power_var_init (A,loc,val);
set inv = power_inv (A,loc,b0,n0);
set Di = denaming (V,A,(val . 1));
set Dj = denaming (V,A,(val . 2));
set Db = denaming (V,A,(val . 3));
set Dn = denaming (V,A,(val . 4));
set Ds = denaming (V,A,(val . 5));
set asi = SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1));
set asj = SC_assignment ((denaming (V,A,(val . 2))),(loc /. 2));
set asb = SC_assignment ((denaming (V,A,(val . 3))),(loc /. 3));
set asn = SC_assignment ((denaming (V,A,(val . 4))),(loc /. 4));
set ass = SC_assignment ((denaming (V,A,(val . 5))),(loc /. 5));
set T1 = SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5));
set S1 = SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4));
set R1 = SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3));
set Q1 = SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2));
set P1 = SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1));
assume that
A1:
not V is empty
and
A2:
A is_without_nonatomicND_wrt V
and
A3:
loc /. 1,loc /. 2,loc /. 3,loc /. 4,loc /. 5 are_mutually_distinct
and
A4:
loc,val are_compatible_wrt_5_locs
; <*(valid_power_input (V,A,val,b0,n0)),(power_var_init (A,loc,val)),(power_inv (A,loc,b0,n0))*> is SFHT of (ND (V,A))
A5:
<*(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))),(SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1))),(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2)))*> is SFHT of (ND (V,A))
by NOMIN_3:29;
A6:
<*(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(SC_assignment ((denaming (V,A,(val . 2))),(loc /. 2))),(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3)))*> is SFHT of (ND (V,A))
by NOMIN_3:29;
A7:
<*(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(SC_assignment ((denaming (V,A,(val . 3))),(loc /. 3))),(SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4)))*> is SFHT of (ND (V,A))
by NOMIN_3:29;
A8:
<*(SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(SC_assignment ((denaming (V,A,(val . 4))),(loc /. 4))),(SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5)))*> is SFHT of (ND (V,A))
by NOMIN_3:29;
A9:
<*(SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(SC_assignment ((denaming (V,A,(val . 5))),(loc /. 5))),(power_inv (A,loc,b0,n0))*> is SFHT of (ND (V,A))
by NOMIN_3:29;
valid_power_input (V,A,val,b0,n0) ||= SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))
proof
let d be
Element of
ND (
V,
A);
NOMIN_3:def 3 ( not d in dom (valid_power_input (V,A,val,b0,n0)) or not (valid_power_input (V,A,val,b0,n0)) . d = TRUE or ( d in dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))) & (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))) . d = TRUE ) )
assume
(
d in dom (valid_power_input (V,A,val,b0,n0)) &
(valid_power_input (V,A,val,b0,n0)) . d = TRUE )
;
( d in dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))) & (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))) . d = TRUE )
then
valid_power_input_pred V,
A,
val,
b0,
n0,
d
by Def8;
then consider d1 being
NonatomicND of
V,
A such that A10:
d = d1
and A11:
{(val . 1),(val . 2),(val . 3),(val . 4),(val . 5)} c= dom d1
and A12:
d1 . (val . 1) = 0
and A13:
d1 . (val . 2) = 1
and A14:
d1 . (val . 3) = b0
and A15:
d1 . (val . 4) = n0
and A16:
d1 . (val . 5) = 1
;
A17:
val . 1
in {(val . 1),(val . 2),(val . 3),(val . 4),(val . 5)}
by ENUMSET1:def 3;
A18:
val . 2
in {(val . 1),(val . 2),(val . 3),(val . 4),(val . 5)}
by ENUMSET1:def 3;
A19:
val . 3
in {(val . 1),(val . 2),(val . 3),(val . 4),(val . 5)}
by ENUMSET1:def 3;
A20:
val . 4
in {(val . 1),(val . 2),(val . 3),(val . 4),(val . 5)}
by ENUMSET1:def 3;
A21:
val . 5
in {(val . 1),(val . 2),(val . 3),(val . 4),(val . 5)}
by ENUMSET1:def 3;
A23:
dom (denaming (V,A,(val . 1))) = { d where d is NonatomicND of V,A : val . 1 in dom d }
by NOMIN_1:def 18;
A24:
dom (denaming (V,A,(val . 2))) = { d where d is NonatomicND of V,A : val . 2 in dom d }
by NOMIN_1:def 18;
A25:
dom (denaming (V,A,(val . 3))) = { d where d is NonatomicND of V,A : val . 3 in dom d }
by NOMIN_1:def 18;
A26:
dom (denaming (V,A,(val . 4))) = { d where d is NonatomicND of V,A : val . 4 in dom d }
by NOMIN_1:def 18;
A27:
dom (denaming (V,A,(val . 5))) = { d where d is NonatomicND of V,A : val . 5 in dom d }
by NOMIN_1:def 18;
A28:
dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,(val . 1))) . d),(loc /. 1)) in dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))) & d in dom (denaming (V,A,(val . 1))) ) }
by NOMIN_2:def 11;
A29:
dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,(val . 2))) . d),(loc /. 2)) in dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))) & d in dom (denaming (V,A,(val . 2))) ) }
by NOMIN_2:def 11;
A30:
dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,(val . 3))) . d),(loc /. 3)) in dom (SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))) & d in dom (denaming (V,A,(val . 3))) ) }
by NOMIN_2:def 11;
A31:
dom (SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,(val . 4))) . d),(loc /. 4)) in dom (SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))) & d in dom (denaming (V,A,(val . 4))) ) }
by NOMIN_2:def 11;
A32:
dom (SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,(val . 5))) . d),(loc /. 5)) in dom (power_inv (A,loc,b0,n0)) & d in dom (denaming (V,A,(val . 5))) ) }
by NOMIN_2:def 11;
reconsider Li =
local_overlapping (
V,
A,
d1,
((denaming (V,A,(val . 1))) . d1),
(loc /. 1)) as
NonatomicND of
V,
A by NOMIN_2:9;
reconsider Lj =
local_overlapping (
V,
A,
Li,
((denaming (V,A,(val . 2))) . Li),
(loc /. 2)) as
NonatomicND of
V,
A by NOMIN_2:9;
reconsider Lb =
local_overlapping (
V,
A,
Lj,
((denaming (V,A,(val . 3))) . Lj),
(loc /. 3)) as
NonatomicND of
V,
A by NOMIN_2:9;
reconsider Ln =
local_overlapping (
V,
A,
Lb,
((denaming (V,A,(val . 4))) . Lb),
(loc /. 4)) as
NonatomicND of
V,
A by NOMIN_2:9;
reconsider Ls =
local_overlapping (
V,
A,
Ln,
((denaming (V,A,(val . 5))) . Ln),
(loc /. 5)) as
NonatomicND of
V,
A by NOMIN_2:9;
A33:
d1 in dom (denaming (V,A,(val . 1)))
by A11, A17, A23;
then A34:
(denaming (V,A,(val . 1))) . d1 is
TypeSCNominativeData of
V,
A
by PARTFUN1:4, NOMIN_1:39;
then A35:
dom Li = {(loc /. 1)} \/ (dom d1)
by A1, A2, NOMIN_4:4;
dom (power_inv (A,loc,b0,n0)) = ND (
V,
A)
by Def12;
then A36:
Ls in dom (power_inv (A,loc,b0,n0))
;
A37:
val . 2
in dom Li
by A11, A18, A35, XBOOLE_0:def 3;
then A38:
Li in dom (denaming (V,A,(val . 2)))
by A24;
then A39:
(denaming (V,A,(val . 2))) . Li is
TypeSCNominativeData of
V,
A
by PARTFUN1:4, NOMIN_1:39;
then A40:
dom Lj = {(loc /. 2)} \/ (dom Li)
by A1, A2, NOMIN_4:4;
A41:
val . 3
in dom Li
by A11, A19, A35, XBOOLE_0:def 3;
then A42:
val . 3
in dom Lj
by A40, XBOOLE_0:def 3;
then A43:
Lj in dom (denaming (V,A,(val . 3)))
by A25;
then A44:
(denaming (V,A,(val . 3))) . Lj is
TypeSCNominativeData of
V,
A
by PARTFUN1:4, NOMIN_1:39;
then A45:
dom Lb = {(loc /. 3)} \/ (dom Lj)
by A1, A2, NOMIN_4:4;
A46:
val . 4
in dom Li
by A11, A20, A35, XBOOLE_0:def 3;
then A47:
val . 4
in dom Lj
by A40, XBOOLE_0:def 3;
then A48:
val . 4
in dom Lb
by A45, XBOOLE_0:def 3;
then A49:
Lb in dom (denaming (V,A,(val . 4)))
by A26;
then A50:
(denaming (V,A,(val . 4))) . Lb is
TypeSCNominativeData of
V,
A
by PARTFUN1:4, NOMIN_1:39;
then A51:
dom Ln = {(loc /. 4)} \/ (dom Lb)
by A1, A2, NOMIN_4:4;
A52:
val . 5
in dom Li
by A11, A21, A35, XBOOLE_0:def 3;
then A53:
val . 5
in dom Lj
by A40, XBOOLE_0:def 3;
then A54:
val . 5
in dom Lb
by A45, XBOOLE_0:def 3;
then A55:
val . 5
in dom Ln
by A51, XBOOLE_0:def 3;
then A56:
Ln in dom (denaming (V,A,(val . 5)))
by A27;
then A57:
Ln in dom (SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5)))
by A32, A36;
then A58:
Lb in dom (SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4)))
by A31, A49;
then A59:
Lj in dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3)))
by A30, A43;
then A60:
Li in dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2)))
by A29, A38;
hence A61:
d in dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1)))
by A10, A28, A33;
(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))) . d = TRUE
A62:
power_inv_pred A,
loc,
b0,
n0,
Ls
proof
take
Ls
;
NOMIN_6:def 11 ( Ls = Ls & {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5)} c= dom Ls & Ls . (loc /. 2) = 1 & Ls . (loc /. 3) = b0 & Ls . (loc /. 4) = n0 & ex S being Complex ex I being Nat st
( I = Ls . (loc /. 1) & S = Ls . (loc /. 5) & S = b0 |^ I ) )
thus
Ls = Ls
;
( {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5)} c= dom Ls & Ls . (loc /. 2) = 1 & Ls . (loc /. 3) = b0 & Ls . (loc /. 4) = n0 & ex S being Complex ex I being Nat st
( I = Ls . (loc /. 1) & S = Ls . (loc /. 5) & S = b0 |^ I ) )
A63:
(denaming (V,A,(val . 5))) . Ln is
TypeSCNominativeData of
V,
A
by A56, PARTFUN1:4, NOMIN_1:39;
then A64:
dom Ls = {(loc /. 5)} \/ (dom Ln)
by A1, A2, NOMIN_4:4;
loc /. 1
in {(loc /. 1)}
by TARSKI:def 1;
then A65:
loc /. 1
in dom Li
by A35, XBOOLE_0:def 3;
then A66:
loc /. 1
in dom Lj
by A40, XBOOLE_0:def 3;
then A67:
loc /. 1
in dom Lb
by A45, XBOOLE_0:def 3;
then
loc /. 1
in dom Ln
by A51, XBOOLE_0:def 3;
then A68:
loc /. 1
in dom Ls
by A64, XBOOLE_0:def 3;
loc /. 2
in {(loc /. 2)}
by TARSKI:def 1;
then A69:
loc /. 2
in dom Lj
by A40, XBOOLE_0:def 3;
then A70:
loc /. 2
in dom Lb
by A45, XBOOLE_0:def 3;
then A71:
loc /. 2
in dom Ln
by A51, XBOOLE_0:def 3;
then A72:
loc /. 2
in dom Ls
by A64, XBOOLE_0:def 3;
loc /. 3
in {(loc /. 3)}
by TARSKI:def 1;
then A73:
loc /. 3
in dom Lb
by A45, XBOOLE_0:def 3;
then A74:
loc /. 3
in dom Ln
by A51, XBOOLE_0:def 3;
then A75:
loc /. 3
in dom Ls
by A64, XBOOLE_0:def 3;
loc /. 4
in {(loc /. 4)}
by TARSKI:def 1;
then
loc /. 4
in dom Ln
by A51, XBOOLE_0:def 3;
then A76:
loc /. 4
in dom Ls
by A64, XBOOLE_0:def 3;
loc /. 5
in {(loc /. 5)}
by TARSKI:def 1;
then
loc /. 5
in dom Ls
by A64, XBOOLE_0:def 3;
hence
{(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5)} c= dom Ls
by A68, A72, A75, A76, ENUMSET1:def 3;
( Ls . (loc /. 2) = 1 & Ls . (loc /. 3) = b0 & Ls . (loc /. 4) = n0 & ex S being Complex ex I being Nat st
( I = Ls . (loc /. 1) & S = Ls . (loc /. 5) & S = b0 |^ I ) )
thus Ls . (loc /. 2) =
Ln . (loc /. 2)
by A1, A2, A3, A63, A71, NOMIN_5:3
.=
Lb . (loc /. 2)
by A1, A2, A3, A50, A70, NOMIN_5:3
.=
Lj . (loc /. 2)
by A1, A2, A3, A44, A69, NOMIN_5:3
.=
(denaming (V,A,(val . 2))) . Li
by A1, A39, NOMIN_2:10
.=
denaming (
(val . 2),
Li)
by A38, NOMIN_1:def 18
.=
Li . (val . 2)
by A37, NOMIN_1:def 12
.=
1
by A1, A2, A11, A4, A18, A13, A34, NOMIN_5:3
;
( Ls . (loc /. 3) = b0 & Ls . (loc /. 4) = n0 & ex S being Complex ex I being Nat st
( I = Ls . (loc /. 1) & S = Ls . (loc /. 5) & S = b0 |^ I ) )
thus Ls . (loc /. 3) =
Ln . (loc /. 3)
by A1, A2, A3, A63, A74, NOMIN_5:3
.=
Lb . (loc /. 3)
by A1, A2, A3, A50, A73, NOMIN_5:3
.=
(denaming (V,A,(val . 3))) . Lj
by A1, A44, NOMIN_2:10
.=
denaming (
(val . 3),
Lj)
by A43, NOMIN_1:def 18
.=
Lj . (val . 3)
by A42, NOMIN_1:def 12
.=
Li . (val . 3)
by A1, A2, A4, A39, A41, NOMIN_5:3
.=
b0
by A1, A2, A11, A19, A14, A34, A4, NOMIN_5:3
;
( Ls . (loc /. 4) = n0 & ex S being Complex ex I being Nat st
( I = Ls . (loc /. 1) & S = Ls . (loc /. 5) & S = b0 |^ I ) )
thus Ls . (loc /. 4) =
Ln . (loc /. 4)
by A1, A2, A3, A11, A18, A19, A20, A21, A33, Th2
.=
(denaming (V,A,(val . 4))) . Lb
by A1, A50, NOMIN_2:10
.=
denaming (
(val . 4),
Lb)
by A49, NOMIN_1:def 18
.=
Lb . (val . 4)
by A48, NOMIN_1:def 12
.=
Lj . (val . 4)
by A1, A2, A4, A44, A47, NOMIN_5:3
.=
Li . (val . 4)
by A1, A2, A4, A39, A46, NOMIN_5:3
.=
n0
by A1, A2, A11, A20, A15, A4, A34, NOMIN_5:3
;
ex S being Complex ex I being Nat st
( I = Ls . (loc /. 1) & S = Ls . (loc /. 5) & S = b0 |^ I )
A78:
Ln . (val . 5) =
Lb . (val . 5)
by A1, A2, A4, A50, A54, NOMIN_5:3
.=
Lj . (val . 5)
by A1, A2, A4, A44, A53, NOMIN_5:3
.=
Li . (val . 5)
by A1, A2, A39, A4, A52, NOMIN_5:3
.=
1
by A1, A2, A11, A21, A16, A34, A4, NOMIN_5:3
;
take
1
;
ex I being Nat st
( I = Ls . (loc /. 1) & 1 = Ls . (loc /. 5) & 1 = b0 |^ I )
take
0
;
( 0 = Ls . (loc /. 1) & 1 = Ls . (loc /. 5) & 1 = b0 |^ 0 )
thus Ls . (loc /. 1) =
Ln . (loc /. 1)
by A1, A2, A11, A3, A18, A19, A20, A21, A33, Th3
.=
Lb . (loc /. 1)
by A1, A2, A50, A3, A67, NOMIN_5:3
.=
Lj . (loc /. 1)
by A1, A2, A66, A3, A44, NOMIN_5:3
.=
Li . (loc /. 1)
by A1, A2, A39, A3, A65, NOMIN_5:3
.=
(denaming (V,A,(val . 1))) . d1
by A1, A34, NOMIN_2:10
.=
denaming (
(val . 1),
d1)
by A33, NOMIN_1:def 18
.=
0
by A11, A12, A17, NOMIN_1:def 12
;
( 1 = Ls . (loc /. 5) & 1 = b0 |^ 0 )
thus Ls . (loc /. 5) =
(denaming (V,A,(val . 5))) . Ln
by A1, A63, NOMIN_2:10
.=
denaming (
(val . 5),
Ln)
by A56, NOMIN_1:def 18
.=
1
by A78, A55, NOMIN_1:def 12
;
1 = b0 |^ 0
thus
1
= b0 |^ 0
by NEWTON:4;
verum
end;
thus (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))) . d =
(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))) . Li
by A10, A61, NOMIN_2:35
.=
(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))) . Lj
by A60, NOMIN_2:35
.=
(SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))) . Lb
by A59, NOMIN_2:35
.=
(SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))) . Ln
by A58, NOMIN_2:35
.=
(power_inv (A,loc,b0,n0)) . Ls
by A57, NOMIN_2:35
.=
TRUE
by A36, A62, Def12
;
verum
end;
then A79:
<*(valid_power_input (V,A,val,b0,n0)),(SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1))),(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2)))*> is SFHT of (ND (V,A))
by A5, NOMIN_3:15;
A80:
<*(PP_inversion (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2)))),(SC_assignment ((denaming (V,A,(val . 2))),(loc /. 2))),(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3)))*> is SFHT of (ND (V,A))
by NOMIN_4:16;
A81:
<*(PP_inversion (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3)))),(SC_assignment ((denaming (V,A,(val . 3))),(loc /. 3))),(SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4)))*> is SFHT of (ND (V,A))
by NOMIN_4:16;
A82:
<*(PP_inversion (SC_Psuperpos ((SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5))),(denaming (V,A,(val . 4))),(loc /. 4)))),(SC_assignment ((denaming (V,A,(val . 4))),(loc /. 4))),(SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5)))*> is SFHT of (ND (V,A))
by NOMIN_4:16;
<*(PP_inversion (SC_Psuperpos ((power_inv (A,loc,b0,n0)),(denaming (V,A,(val . 5))),(loc /. 5)))),(SC_assignment ((denaming (V,A,(val . 5))),(loc /. 5))),(power_inv (A,loc,b0,n0))*> is SFHT of (ND (V,A))
by NOMIN_4:16;
hence
<*(valid_power_input (V,A,val,b0,n0)),(power_var_init (A,loc,val)),(power_inv (A,loc,b0,n0))*> is SFHT of (ND (V,A))
by A79, A6, A7, A8, A9, A80, A81, A82, Th1; verum