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

( ( 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

hence
f1 = f2
by A8, A9, FUNCT_1:2; :: thesis: verum
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 ;

end;assume k in NAT ; :: thesis: f1 . k = f2 . k

then reconsider k9 = k as Element of NAT ;