let f1, f2 be Function of NAT ,S; :: thesis: ( ( for i being Element of NAT holds
( ( ex k being Element of NAT st i = 2 * k implies f1 . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies f1 . i = b ) ) ) & ( for i being Element of NAT holds
( ( ex k being Element of NAT st i = 2 * k implies f2 . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies f2 . i = b ) ) ) implies f1 = f2 )
A6: ( dom f1 = NAT & dom f2 = NAT ) by FUNCT_2:def 1;
assume that
A7: for i being Element of NAT holds
( ( ex k being Element of NAT st i = 2 * k implies f1 . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies f1 . i = b ) ) and
A8: for i being Element of NAT holds
( ( ex k being Element of NAT st i = 2 * k implies f2 . i = a ) & ( ( for k being Element of NAT holds not i = 2 * k ) implies f2 . i = b ) ) ; :: thesis: f1 = f2
for k being set st k in NAT holds
f1 . k = f2 . k

proof

let k be set ; :: thesis: ( k in NAT implies f1 . k = f2 . k )
assume k in NAT ; :: thesis: f1 . k = f2 . k
then reconsider k' = k as Element of NAT ;

per cases ( ex l being Element of NAT st k = 2 * l or for l being Element of NAT holds not k = 2 * l ) ;

suppose A9: ex l being Element of NAT st k = 2 * l ; :: thesis: f1 . k = f2 . k

then f1 . k = a by A7
.= f2 . k by A8, A9 ;
hence f1 . k = f2 . k ; :: thesis: verum

end;

suppose A10: for l being Element of NAT holds not k = 2 * l ; :: thesis: f1 . k = f2 . k

then f1 . k' = b by A7
.= f2 . k' by A8, A10 ;
hence f1 . k = f2 . k ; :: thesis: verum

end;

end;

end;

hence f1 = f2 by A6, FUNCT_1:9; :: thesis: verum