defpred S1[ set ] means ex m being Element of NAT st $1 = 5 * m; consider N being Subset of NAT such that A1:
for n being Element of NAT holds ( n in N iff S1[n] )
fromSUBSET_1:sch 3(); defpred S2[ set ] means ex m being Element of NAT st $1 =(5 * m)+ 1; consider M being Subset of NAT such that A2:
for n being Element of NAT holds ( n in M iff S2[n] )
fromSUBSET_1:sch 3(); defpred S3[ set ] means ex m being Element of NAT st $1 =(5 * m)+ 2; consider K being Subset of NAT such that A3:
for n being Element of NAT holds ( n in K iff S3[n] )
fromSUBSET_1:sch 3(); defpred S4[ set ] means ex m being Element of NAT st $1 =(5 * m)+ 3; consider L being Subset of NAT such that A4:
for n being Element of NAT holds ( n in L iff S4[n] )
fromSUBSET_1:sch 3(); defpred S5[ set ] means ex m being Element of NAT st $1 =(5 * m)+ 4; consider O being Subset of NAT such that A5:
for n being Element of NAT holds ( n in O iff S5[n] )
fromSUBSET_1:sch 3(); defpred S6[ Element of NAT , set ] means ( ( $1 in N implies $2 = F1(($1 / 5)) ) & ( $1 in M implies $2 = F2((($1 - 1)/ 5)) ) & ( $1 in K implies $2 = F3((($1 - 2)/ 5)) ) & ( $1 in L implies $2 = F4((($1 - 3)/ 5)) ) & ( $1 in O implies $2 = F5((($1 - 4)/ 5)) ) ); A6:
for n being Element of NAT ex r being Element of REAL st S6[n,r]