let V, A be set ; :: thesis:
let loc be V -valued 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;
assume that
A1: not V is empty and
A2: A is complex-containing and
A3: A is_without_nonatomicND_wrt V and
A4: loc /. 1,loc /. 2,loc /. 3,loc /. 4,loc /. 5 are_mutually_distinct ; :: thesis:
set D = ND (V,A);
set inv = power_inv (A,loc,b0,n0);
set L = power_loop_body (A,loc);
set add = addition (A,(loc /. 1),(loc /. 2));
set mlt = multiplication (A,(loc /. 5),(loc /. 3));
set f = SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1));
set g = SC_assignment ((multiplication (A,(loc /. 5),(loc /. 3))),(loc /. 5));
set Di = denaming (V,A,(loc /. 1));
set Dj = denaming (V,A,(loc /. 2));
set Db = denaming (V,A,(loc /. 3));
set Dn = denaming (V,A,(loc /. 4));
set Ds = denaming (V,A,(loc /. 5));

now :: thesis:

let d be TypeSCNominativeData of V,A; :: thesis:
assume that
A5: d in dom (power_inv (A,loc,b0,n0)) and
A6: (power_inv (A,loc,b0,n0)) . d = TRUE and
A7: d in dom (power_loop_body (A,loc)) and
A8: (power_loop_body (A,loc)) . d in dom (power_inv (A,loc,b0,n0)) ; :: thesis:
power_inv_pred A,loc,b0,n0,d by A5, A6, Def12;
then consider d1 being NonatomicND of V,A such that
A9: d = d1 and
A10: {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5)} c= dom d1 and
A11: d1 . (loc /. 2) = 1 and
A12: d1 . (loc /. 3) = b0 and
A13: d1 . (loc /. 4) = n0 and
A14: ex S being Complex ex I being Nat st
( I = d1 . (loc /. 1) & S = d1 . (loc /. 5) & S = b0 |^ I ) ;
A15: loc /. 1 in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5)} by ENUMSET1:def 3;
A16: loc /. 2 in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5)} by ENUMSET1:def 3;
A17: loc /. 3 in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5)} by ENUMSET1:def 3;
A18: loc /. 4 in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5)} by ENUMSET1:def 3;
A19: loc /. 5 in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5)} by ENUMSET1:def 3;
consider S being Complex, I being Nat such that
A20: I = d1 . (loc /. 1) and
A22: S = d1 . (loc /. 5) and
A23: S = b0 |^ I by A14;
A24: dom (SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) = dom (addition (A,(loc /. 1),(loc /. 2))) by NOMIN_2:def 7;
A25: dom (SC_assignment ((multiplication (A,(loc /. 5),(loc /. 3))),(loc /. 5))) = dom (multiplication (A,(loc /. 5),(loc /. 3))) by NOMIN_2:def 7;
A26: PP_composition ((SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))),(SC_assignment ((multiplication (A,(loc /. 5),(loc /. 3))),(loc /. 5)))) = (SC_assignment ((multiplication (A,(loc /. 5),(loc /. 3))),(loc /. 5))) * (SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) by PARTPR_2:def 1;
then A27: d in dom (SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) by A7, FUNCT_1:11;
then reconsider Ad = (addition (A,(loc /. 1),(loc /. 2))) . d1 as TypeSCNominativeData of V,A by A24, A9, PARTFUN1:4, NOMIN_1:39;
reconsider La = local_overlapping (V,A,d1,Ad,(loc /. 1)) as NonatomicND of V,A by NOMIN_2:9;
reconsider Lm = local_overlapping (V,A,La,((multiplication (A,(loc /. 5),(loc /. 3))) . La),(loc /. 5)) as NonatomicND of V,A by NOMIN_2:9;
power_loop_body (A,loc) = (SC_assignment ((multiplication (A,(loc /. 5),(loc /. 3))),(loc /. 5))) * (SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) by PARTPR_2:def 1;
then A28: (power_loop_body (A,loc)) . d = (SC_assignment ((multiplication (A,(loc /. 5),(loc /. 3))),(loc /. 5))) . ((SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) . d) by A7, FUNCT_1:12;
A29: (SC_assignment ((addition (A,(loc /. 1),(loc /. 2))),(loc /. 1))) . d = La by A9, A27, NOMIN_2:def 7;
then A30: La in dom (SC_assignment ((multiplication (A,(loc /. 5),(loc /. 3))),(loc /. 5))) by A7, A26, FUNCT_1:11;
A31: (SC_assignment ((multiplication (A,(loc /. 5),(loc /. 3))),(loc /. 5))) . La = Lm by A30, NOMIN_2:def 7;
power_inv_pred A,loc,b0,n0,Lm

proof

take Lm ; :: according to NOMIN_6:def 11 :: thesis:
thus Lm = Lm ; :: thesis:
A32: (multiplication (A,(loc /. 5),(loc /. 3))) . La is TypeSCNominativeData of V,A by A25, A30, PARTFUN1:4, NOMIN_1:39;
A33: dom Lm = (dom La) \/ {(loc /. 5)} by A3, A1, A25, A30, A31, NOMIN_4:5;
A34: dom La = {(loc /. 1)} \/ (dom d1) by A3, A1, NOMIN_4:4;
loc /. 1 in {(loc /. 1)} by TARSKI:def 1;
then A35: loc /. 1 in dom La by A34, XBOOLE_0:def 3;
then A36: loc /. 1 in dom Lm by A33, XBOOLE_0:def 3;
A37: loc /. 2 in dom La by A10, A16, A34, XBOOLE_0:def 3;
then A38: loc /. 2 in dom Lm by A33, XBOOLE_0:def 3;
A39: loc /. 3 in dom La by A17, A10, A34, XBOOLE_0:def 3;
then A40: loc /. 3 in dom Lm by A33, XBOOLE_0:def 3;
A41: loc /. 4 in dom La by A10, A18, A34, XBOOLE_0:def 3;
then A42: loc /. 4 in dom Lm by A33, XBOOLE_0:def 3;
loc /. 5 in {(loc /. 5)} by TARSKI:def 1;
then loc /. 5 in dom Lm by A33, XBOOLE_0:def 3;
hence {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5)} c= dom Lm by A36, A38, A40, A42, ENUMSET1:def 3; :: thesis:
thus Lm . (loc /. 2) = La . (loc /. 2) by A1, A32, A3, A4, A37, NOMIN_5:3
.= 1 by A3, A1, A10, A16, A11, A4, NOMIN_5:3 ; :: thesis:
thus Lm . (loc /. 3) = La . (loc /. 3) by A1, A4, A32, A39, A3, NOMIN_5:3
.= b0 by A3, A1, A10, A4, A17, A12, NOMIN_5:3 ; :: thesis:
thus Lm . (loc /. 4) = La . (loc /. 4) by A4, A1, A32, A41, A3, NOMIN_5:3
.= n0 by A10, A3, A1, A4, A18, A13, NOMIN_5:3 ; :: thesis:
take S1 = S * b0; :: thesis:
take I1 = I + 1; :: thesis:
La . (loc /. 1) = Ad by A1, NOMIN_2:10
.= I1 by A15, A2, A10, A20, A11, A16, A9, A27, A24, NOMIN_5:4 ;
hence Lm . (loc /. 1) = I1 by A1, A32, A3, A4, A35, NOMIN_5:3; :: thesis:
A43: loc /. 5 in dom La by A10, A19, A34, XBOOLE_0:def 3;
A44: La . (loc /. 5) = d1 . (loc /. 5) by A3, A1, A10, A4, A19, NOMIN_5:3;
A45: La . (loc /. 3) = d1 . (loc /. 3) by A3, A1, A10, A4, A17, NOMIN_5:3;
thus Lm . (loc /. 5) = (multiplication (A,(loc /. 5),(loc /. 3))) . La by A1, A32, NOMIN_2:10
.= S1 by A39, A12, A45, A2, A22, A43, A25, A30, A44, NOMIN_5:5 ; :: thesis:
thus S1 = b0 |^ I1 by A23, NEWTON:6; :: thesis:

end;

hence (power_inv (A,loc,b0,n0)) . ((power_loop_body (A,loc)) . d) = TRUE by A8, A28, A29, A31, Def12; :: thesis:

end;

hence <*(power_inv (A,loc,b0,n0)),(power_loop_body (A,loc)),(power_inv (A,loc,b0,n0))*> is SFHT of (ND (V,A)) by NOMIN_3:28; :: thesis: