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:
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 D = ND (V,A);
set inv = power_inv (A,loc,b0,n0);
set O = valid_power_output (A,z,b0,n0);
set Di = denaming (V,A,(loc /. 1));
set Dn = denaming (V,A,(loc /. 4));
set Ds = denaming (V,A,(loc /. 5));
set g = SC_assignment ((denaming (V,A,(loc /. 5))),z);
set E = Equality (A,(loc /. 1),(loc /. 4));
set q = PP_and ((Equality (A,(loc /. 1),(loc /. 4))),(power_inv (A,loc,b0,n0)));
set P = PP_inversion (PP_and ((Equality (A,(loc /. 1),(loc /. 4))),(power_inv (A,loc,b0,n0))));
assume A1: ( ( for T being TypeSCNominativeData of V,A holds loc /. 1 is_a_value_on T ) & ( for T being TypeSCNominativeData of V,A holds loc /. 4 is_a_value_on T ) ) ; :: thesis:

now :: thesis:

let d be TypeSCNominativeData of V,A; :: thesis:
assume that
A2: d in dom (PP_inversion (PP_and ((Equality (A,(loc /. 1),(loc /. 4))),(power_inv (A,loc,b0,n0))))) and
(PP_inversion (PP_and ((Equality (A,(loc /. 1),(loc /. 4))),(power_inv (A,loc,b0,n0))))) . d = TRUE and
d in dom (SC_assignment ((denaming (V,A,(loc /. 5))),z)) and
(SC_assignment ((denaming (V,A,(loc /. 5))),z)) . d in dom (valid_power_output (A,z,b0,n0)) ; :: thesis:
A3: dom (PP_and ((Equality (A,(loc /. 1),(loc /. 4))),(power_inv (A,loc,b0,n0)))) = { d where d is Element of ND (V,A) : ( ( d in dom (Equality (A,(loc /. 1),(loc /. 4))) & (Equality (A,(loc /. 1),(loc /. 4))) . d = FALSE ) or ( d in dom (power_inv (A,loc,b0,n0)) & (power_inv (A,loc,b0,n0)) . d = FALSE ) or ( d in dom (Equality (A,(loc /. 1),(loc /. 4))) & (Equality (A,(loc /. 1),(loc /. 4))) . d = TRUE & d in dom (power_inv (A,loc,b0,n0)) & (power_inv (A,loc,b0,n0)) . d = TRUE ) ) } by PARTPR_1:16;
A4: dom (denaming (V,A,(loc /. 1))) = { d where d is NonatomicND of V,A : loc /. 1 in dom d } by NOMIN_1:def 18;
A5: dom (denaming (V,A,(loc /. 4))) = { d where d is NonatomicND of V,A : loc /. 4 in dom d } by NOMIN_1:def 18;
A6: dom (Equality (A,(loc /. 1),(loc /. 4))) = (dom (denaming (V,A,(loc /. 1)))) /\ (dom (denaming (V,A,(loc /. 4)))) by A1, NOMIN_4:11;
A7: not d in dom (PP_and ((Equality (A,(loc /. 1),(loc /. 4))),(power_inv (A,loc,b0,n0)))) by A2, PARTPR_2:9;
dom (Equality (A,(loc /. 1),(loc /. 4))) c= dom (PP_and ((Equality (A,(loc /. 1),(loc /. 4))),(power_inv (A,loc,b0,n0)))) by PARTPR_2:3;
then not d in dom (Equality (A,(loc /. 1),(loc /. 4))) by A2, PARTPR_2:9;
then A8: ( not d in dom (denaming (V,A,(loc /. 1))) or not d in dom (denaming (V,A,(loc /. 4))) ) by A6, XBOOLE_0:def 4;
dom (power_inv (A,loc,b0,n0)) = ND (V,A) by Def12;
then A9: d in dom (power_inv (A,loc,b0,n0)) ;
then (power_inv (A,loc,b0,n0)) . d <> FALSE by A3, A7;
then power_inv_pred A,loc,b0,n0,d by A9, Def12;
then consider d1 being NonatomicND of V,A such that
A10: ( d = d1 & {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5)} c= dom d1 ) and
( d1 . (loc /. 2) = 1 & d1 . (loc /. 3) = b0 & d1 . (loc /. 4) = n0 & ex S being Complex ex I being Nat st
( I = d1 . (loc /. 1) & S = d1 . (loc /. 5) & S = b0 |^ I ) ) ;
( loc /. 1 in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5)} & loc /. 4 in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5)} ) by ENUMSET1:def 3;
hence (valid_power_output (A,z,b0,n0)) . ((SC_assignment ((denaming (V,A,(loc /. 5))),z)) . d) = TRUE by A4, A5, A8, A10; :: thesis:

end;

hence <*(PP_inversion (PP_and ((Equality (A,(loc /. 1),(loc /. 4))),(power_inv (A,loc,b0,n0))))),(SC_assignment ((denaming (V,A,(loc /. 5))),z)),(valid_power_output (A,z,b0,n0))*> is SFHT of (ND (V,A)) by NOMIN_3:28; :: thesis: