let f1, f2 be sequence of REAL; :: thesis: ( ( for i being Nat holds
( ( i in X & f1 . i = r |^ i ) or ( not i in X & f1 . i = 0 ) ) ) & ( for i being Nat holds
( ( i in X & f2 . i = r |^ i ) or ( not i in X & f2 . i = 0 ) ) ) implies f1 = f2 )
assume that
A3: for i being Nat holds
( ( i in X & f1 . i = r |^ i ) or ( not i in X & f1 . i = 0 ) ) and
A4: for i being Nat holds
( ( i in X & f2 . i = r |^ i ) or ( not i in X & f2 . i = 0 ) ) ; :: thesis: f1 = f2

now :: thesis: for i being Element of NAT holds f1 . i = f2 . i

let i be Element of NAT ; :: thesis: f1 . i = f2 . i
( ( i in X & f1 . i = r |^ i ) or ( not i in X & f1 . i = 0 ) ) by A3;
hence f1 . i = f2 . i by A4; :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:63; :: thesis: verum