let f1, f2 be sequence of 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 )
A8: dom f1 = NAT by FUNCT_2:def 1;
A9: dom f2 = NAT by FUNCT_2:def 1;
assume that
A10: 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
A11: 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 object st k in NAT holds
f1 . k = f2 . k
proof
let k be object ; :: thesis: ( k in NAT implies f1 . k = f2 . k )
assume k in NAT ; :: thesis: f1 . k = f2 . k
then reconsider k9 = 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 A12: ex l being Element of NAT st k = 2 * l ; :: thesis: f1 . k = f2 . k
then f1 . k = a by A10
.= f2 . k by A11, A12 ;
hence f1 . k = f2 . k ; :: thesis: verum
end;
suppose A13: for l being Element of NAT holds not k = 2 * l ; :: thesis: f1 . k = f2 . k
then f1 . k9 = b by A10
.= f2 . k9 by A11, A13 ;
hence f1 . k = f2 . k ; :: thesis: verum
end;
end;
end;
hence f1 = f2 by A8, A9, FUNCT_1:2; :: thesis: verum