let V, A be set ; :: thesis:
let loc be V -valued Function; :: thesis:
let val be Function; :: thesis:
let n0 be Nat; :: thesis:
let b0 be Complex; :: thesis:
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 ; :: thesis:
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); :: according to NOMIN_3:def 3 :: thesis:
assume ( d in dom (valid_power_input (V,A,val,b0,n0)) & (valid_power_input (V,A,val,b0,n0)) . d = TRUE ) ; :: thesis:
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; :: thesis:
A62: power_inv_pred A,loc,b0,n0,Ls

proof

take Ls ; :: according to NOMIN_6:def 11 :: thesis:
thus Ls = Ls ; :: thesis:
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; :: thesis:
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 ; :: thesis:
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 ; :: thesis:
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 ; :: thesis:
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 ; :: thesis:
take 0 ; :: thesis:
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 ; :: thesis:
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 ; :: thesis:
thus 1 = b0 |^ 0 by NEWTON:4; :: thesis:

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 ; :: thesis:

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; :: thesis: