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 Di = denaming (V,A,(loc /. 1));
set Db = denaming (V,A,(loc /. 3));
set Dn = denaming (V,A,(loc /. 4));
set Ds = denaming (V,A,(loc /. 5));
set Dz = denaming (V,A,z);
set ass = SC_assignment ((denaming (V,A,(loc /. 5))),z);
set out = valid_power_output (A,z,b0,n0);
set p = SC_Psuperpos ((valid_power_output (A,z,b0,n0)),(denaming (V,A,(loc /. 5))),z);
set E = Equality (A,(loc /. 1),(loc /. 4));
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 and
A3: for T being TypeSCNominativeData of V,A holds loc /. 4 is_a_value_on T ; :: thesis:
let d be Element of ND (V,A); :: according to NOMIN_3:def 3 :: thesis:
assume that
A4: d in dom (PP_and ((Equality (A,(loc /. 1),(loc /. 4))),(power_inv (A,loc,b0,n0)))) and
A5: (PP_and ((Equality (A,(loc /. 1),(loc /. 4))),(power_inv (A,loc,b0,n0)))) . d = TRUE ; :: thesis:
A6: dom (SC_Psuperpos ((valid_power_output (A,z,b0,n0)),(denaming (V,A,(loc /. 5))),z)) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,(loc /. 5))) . d),z) in dom (valid_power_output (A,z,b0,n0)) & d in dom (denaming (V,A,(loc /. 5))) ) } by NOMIN_2:def 11;
A7: dom (valid_power_output (A,z,b0,n0)) = { d where d is TypeSCNominativeData of V,A : d in dom (denaming (V,A,z)) } by Def10;
A8: dom (denaming (V,A,(loc /. 5))) = { d where d is NonatomicND of V,A : loc /. 5 in dom d } by NOMIN_1:def 18;
A9: dom (denaming (V,A,z)) = { d where d is NonatomicND of V,A : z in dom d } by NOMIN_1:def 18;
A10: d in dom (Equality (A,(loc /. 1),(loc /. 4))) by A4, A5, PARTPR_1:23;
A11: d in dom (power_inv (A,loc,b0,n0)) by A4, A5, PARTPR_1:23;
A12: dom (Equality (A,(loc /. 1),(loc /. 4))) = (dom (denaming (V,A,(loc /. 1)))) /\ (dom (denaming (V,A,(loc /. 4)))) by A2, A3, NOMIN_4:11;
then A13: d in dom (denaming (V,A,(loc /. 1))) by A10, XBOOLE_0:def 4;
(power_inv (A,loc,b0,n0)) . d = TRUE by A4, A5, PARTPR_1:23;
then power_inv_pred A,loc,b0,n0,d by A11, Def12;
then consider d1 being NonatomicND of V,A such that
A14: d = d1 and
A15: {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5)} c= dom d1 and
A16: d1 . (loc /. 4) = n0 and
d1 . (loc /. 3) = b0 and
A18: ex S being Complex ex I being Nat st
( I = d1 . (loc /. 1) & S = d1 . (loc /. 5) & S = b0 |^ I ) ;
A19: loc /. 1 in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5)} by ENUMSET1:def 3;
A20: loc /. 4 in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5)} by ENUMSET1:def 3;
A21: loc /. 5 in {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5)} by ENUMSET1:def 3;
reconsider dd = d as TypeSCNominativeData of V,A by NOMIN_1:39;
set L = local_overlapping (V,A,dd,((denaming (V,A,(loc /. 5))) . dd),z);
A22: dd in dom (denaming (V,A,(loc /. 5))) by A15, A8, A14, A21;
then (denaming (V,A,(loc /. 5))) . d1 in ND (V,A) by A14, PARTFUN1:4;
then A23: ex d2 being TypeSCNominativeData of V,A st (denaming (V,A,(loc /. 5))) . d1 = d2 ;
then A24: local_overlapping (V,A,dd,((denaming (V,A,(loc /. 5))) . dd),z) in dom (denaming (V,A,z)) by A1, A14, NOMIN_4:6;
then A25: local_overlapping (V,A,dd,((denaming (V,A,(loc /. 5))) . dd),z) in dom (valid_power_output (A,z,b0,n0)) by A7;
hence A26: d in dom (SC_Psuperpos ((valid_power_output (A,z,b0,n0)),(denaming (V,A,(loc /. 5))),z)) by A6, A22; :: thesis:
valid_power_output_pred A,z,b0,n0, local_overlapping (V,A,dd,((denaming (V,A,(loc /. 5))) . dd),z)

proof

consider S being Complex, I being Nat such that
A27: I = d1 . (loc /. 1) and
A29: S = d1 . (loc /. 5) and
A30: S = b0 |^ I by A18;
A31: ex d being NonatomicND of V,A st
( local_overlapping (V,A,dd,((denaming (V,A,(loc /. 5))) . dd),z) = d & z in dom d ) by A9, A24;
then reconsider dlo = local_overlapping (V,A,dd,((denaming (V,A,(loc /. 5))) . dd),z) as NonatomicND of V,A ;
take dlo ; :: according to NOMIN_6:def 9 :: thesis:
thus local_overlapping (V,A,dd,((denaming (V,A,(loc /. 5))) . dd),z) = dlo ; :: thesis:
thus z in dom dlo by A31; :: thesis:
A32: loc /. 1 is_a_value_on dd by A2;
A33: loc /. 4 is_a_value_on dd by A3;
A34: dom <:(denaming (V,A,(loc /. 1))),(denaming (V,A,(loc /. 4))):> = (dom (denaming (V,A,(loc /. 1)))) /\ (dom (denaming (V,A,(loc /. 4)))) by FUNCT_3:def 7;
d in dom <:(denaming (V,A,(loc /. 1))),(denaming (V,A,(loc /. 4))):> by A10, A12, FUNCT_3:def 7;
then A35: (Equality (A,(loc /. 1),(loc /. 4))) . d = (Equality A) . (<:(denaming (V,A,(loc /. 1))),(denaming (V,A,(loc /. 4))):> . d) by FUNCT_1:13;
A36: d in dom (denaming (V,A,(loc /. 4))) by A10, A12, XBOOLE_0:def 4;
A37: <:(denaming (V,A,(loc /. 1))),(denaming (V,A,(loc /. 4))):> . d = [((denaming (V,A,(loc /. 1))) . d),((denaming (V,A,(loc /. 4))) . d)] by A10, A12, A34, FUNCT_3:def 7;
A38: (denaming (V,A,(loc /. 1))) . d = denaming ((loc /. 1),d1) by A14, A13, NOMIN_1:def 18
.= d1 . (loc /. 1) by A15, A19, NOMIN_1:def 12 ;
A39: (denaming (V,A,(loc /. 4))) . d = denaming ((loc /. 4),d1) by A14, A36, NOMIN_1:def 18
.= d1 . (loc /. 4) by A15, A20, NOMIN_1:def 12 ;
A40: (denaming (V,A,(loc /. 5))) . d = denaming ((loc /. 5),d1) by A22, A14, NOMIN_1:def 18
.= d1 . (loc /. 5) by A15, A21, NOMIN_1:def 12 ;
(Equality A) . (((denaming (V,A,(loc /. 1))) . d),((denaming (V,A,(loc /. 4))) . d)) <> FALSE by A4, A5, A35, A37, PARTPR_1:23;
then (denaming (V,A,(loc /. 1))) . d = (denaming (V,A,(loc /. 4))) . d by A32, A33, NOMIN_4:def 9;
hence dlo . z = b0 |^ n0 by A1, A14, A16, A23, A27, A29, A30, A38, A39, A40, NOMIN_2:10; :: thesis:

end;

hence TRUE = (valid_power_output (A,z,b0,n0)) . (local_overlapping (V,A,dd,((denaming (V,A,(loc /. 5))) . dd),z)) by A25, Def10
.= (SC_Psuperpos ((valid_power_output (A,z,b0,n0)),(denaming (V,A,(loc /. 5))),z)) . d by A26, NOMIN_2:35 ;
:: thesis: