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

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

hence
f1 = f2
by FUNCT_2:63; :: thesis: verumlet 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;( ( 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