let V, A be set ; :: thesis: for z being Element of V
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 complex-containing & 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 & ( 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 ) holds
<*(valid_power_input (V,A,val,b0,n0)),(power_program (A,loc,val,z)),(valid_power_output (A,z,b0,n0))*> is SFHT of (ND (V,A))
let z be Element of V; :: thesis: 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 complex-containing & 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 & ( 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 ) holds
<*(valid_power_input (V,A,val,b0,n0)),(power_program (A,loc,val,z)),(valid_power_output (A,z,b0,n0))*> is SFHT of (ND (V,A))
let loc be V -valued Function; :: thesis: for val being Function
for n0 being Nat
for b0 being Complex st not V is empty & A is complex-containing & 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 & ( 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 ) holds
<*(valid_power_input (V,A,val,b0,n0)),(power_program (A,loc,val,z)),(valid_power_output (A,z,b0,n0))*> is SFHT of (ND (V,A))
let val be Function; :: thesis: for n0 being Nat
for b0 being Complex st not V is empty & A is complex-containing & 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 & ( 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 ) holds
<*(valid_power_input (V,A,val,b0,n0)),(power_program (A,loc,val,z)),(valid_power_output (A,z,b0,n0))*> is SFHT of (ND (V,A))
let n0 be Nat; :: thesis: for b0 being Complex st not V is empty & A is complex-containing & 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 & ( 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 ) holds
<*(valid_power_input (V,A,val,b0,n0)),(power_program (A,loc,val,z)),(valid_power_output (A,z,b0,n0))*> is SFHT of (ND (V,A))
let b0 be Complex; :: thesis: ( not V is empty & A is complex-containing & 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 & ( 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 ) implies <*(valid_power_input (V,A,val,b0,n0)),(power_program (A,loc,val,z)),(valid_power_output (A,z,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 D = ND (V,A);
set p = valid_power_input (V,A,val,b0,n0);
set f = power_main_part (A,loc,val);
set g = SC_assignment ((denaming (V,A,(loc /. 5))),z);
set q = valid_power_output (A,z,b0,n0);
set inv = power_inv (A,loc,b0,n0);
set E = Equality (A,(loc /. 1),(loc /. 4));
assume that
A1: ( not V is empty & A is complex-containing & A is_without_nonatomicND_wrt V & loc /. 1,loc /. 2,loc /. 3,loc /. 4,loc /. 5 are_mutually_distinct ) and
A2: loc,val are_compatible_wrt_5_locs and
A3: ( ( 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: <*(valid_power_input (V,A,val,b0,n0)),(power_program (A,loc,val,z)),(valid_power_output (A,z,b0,n0))*> is SFHT of (ND (V,A))
A4: <*(valid_power_input (V,A,val,b0,n0)),(power_main_part (A,loc,val)),(PP_and ((Equality (A,(loc /. 1),(loc /. 4))),(power_inv (A,loc,b0,n0))))*> is SFHT of (ND (V,A)) by A1, A2, Th8;
A5: <*(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 A1, A3, Th10;
<*(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 A3, Th11;
hence <*(valid_power_input (V,A,val,b0,n0)),(power_program (A,loc,val,z)),(valid_power_output (A,z,b0,n0))*> is SFHT of (ND (V,A)) by A4, A5, NOMIN_3:25; :: thesis: verum