let n be Nat; :: thesis: { k where k is Nat : k divides 5 |^ n } = divisors ((5 |^ n),4,1)
set A = { k where k is Nat : k divides 5 |^ n } ;
set B = divisors ((5 |^ n),4,1);
thus { k where k is Nat : k divides 5 |^ n } c= divisors ((5 |^ n),4,1) :: according to XBOOLE_0:def 10 :: thesis: divisors ((5 |^ n),4,1) c= { k where k is Nat : k divides 5 |^ n }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Nat : k divides 5 |^ n } or x in divisors ((5 |^ n),4,1) )
assume x in { k where k is Nat : k divides 5 |^ n } ; :: thesis: x in divisors ((5 |^ n),4,1)
then consider k being Nat such that
A1: x = k and
A2: k divides 5 |^ n ;
k mod 4 = 1 by A2, Th34;
hence x in divisors ((5 |^ n),4,1) by A1, A2; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in divisors ((5 |^ n),4,1) or x in { k where k is Nat : k divides 5 |^ n } )
assume x in divisors ((5 |^ n),4,1) ; :: thesis: x in { k where k is Nat : k divides 5 |^ n }
then ex k being Nat st
( x = k & k mod 4 = 1 & k divides 5 |^ n ) ;
hence x in { k where k is Nat : k divides 5 |^ n } ; :: thesis: verum