thus ( F is odd-valued implies for x being object st x in dom F holds
F . x is odd Nat ) :: thesis: ( ( for x being object st x in dom F holds
F . x is odd Nat ) implies F is odd-valued )
proof
assume A1: F is odd-valued ; :: thesis: for x being object st x in dom F holds
F . x is odd Nat
let x be object ; :: thesis: ( x in dom F implies F . x is odd Nat )
assume x in dom F ; :: thesis: F . x is odd Nat
then F . x in rng F by FUNCT_1:def 3;
then F . x in OddNAT by A1;
then ex k being Element of NAT st F . x = (2 * k) + 1 by FIB_NUM2:def 4;
hence F . x is odd Nat ; :: thesis: verum
end;
assume A2: for x being object st x in dom F holds
F . x is odd Nat ; :: thesis: F is odd-valued
rng F c= OddNAT
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng F or y in OddNAT )
assume y in rng F ; :: thesis: y in OddNAT
then consider x being object such that
A3: ( x in dom F & F . x = y ) by FUNCT_1:def 3;
F . x is odd Nat by A2, A3;
then consider i being Nat such that
A4: F . x = (2 * i) + 1 by ABIAN:9;
i in NAT by ORDINAL1:def 12;
hence y in OddNAT by FIB_NUM2:def 4, A3, A4; :: thesis: verum
end;
hence F is odd-valued ; :: thesis: verum