let n be Nat; :: thesis: ( divisors ((2 |^ n),4,3) = {} & divisors ((2 |^ n),4,1) = {1} )
thus divisors ((2 |^ n),4,3) = {} :: thesis: divisors ((2 |^ n),4,1) = {1}

proof

assume divisors ((2 |^ n),4,3) <> {} ; :: thesis: contradiction
then consider k being object such that
A1: k in divisors ((2 |^ n),4,3) by XBOOLE_0:def 1;
reconsider k = k as Nat by A1;
A2: ( k mod 4 = 3 & k divides 2 |^ n ) by A1, Th12;
k <> 1 by A2, PEPIN:5;
hence contradiction by A2, Lm4; :: thesis: verum

end;

( 1 mod 4 = 1 & 1 divides 2 |^ n ) by NAT_D:6, PEPIN:5;
then A3: 1 in divisors ((2 |^ n),4,1) ;
divisors ((2 |^ n),4,1) c= {1}

proof

let k be object ; :: according to TARSKI:def 3 :: thesis: ( not k in divisors ((2 |^ n),4,1) or k in {1} )
assume A4: ( k in divisors ((2 |^ n),4,1) & not k in {1} ) ; :: thesis: contradiction
then reconsider k = k as Nat ;
A5: ( k mod 4 = 1 & k divides 2 |^ n ) by A4, Th12;
k <> 1 by A4, TARSKI:def 1;
hence contradiction by A5, Lm4; :: thesis: verum

end;

hence divisors ((2 |^ n),4,1) = {1} by A3, ZFMISC_1:33; :: thesis: verum