let f be Field-yielding ascending sequence ; :: thesis: for a, b being Element of (SeqField f)
for i being Element of NAT
for x, y being Element of (f . i) st x = a & y = b holds
( a + b = x + y & a * b = x * y )
let a, b be Element of (SeqField f); :: thesis: for i being Element of NAT
for x, y being Element of (f . i) st x = a & y = b holds
( a + b = x + y & a * b = x * y )
let i be Element of NAT ; :: thesis: for x, y being Element of (f . i) st x = a & y = b holds
( a + b = x + y & a * b = x * y )
let x, y be Element of (f . i); :: thesis: ( x = a & y = b implies ( a + b = x + y & a * b = x * y ) )
assume AS: ( x = a & y = b ) ; :: thesis: ( a + b = x + y & a * b = x * y )
H: ( a is Element of Carrier f & b is Element of Carrier f ) by dsf;
then consider j being Element of NAT , xj, yj being Element of (f . j) such that
A: ( xj = a & yj = b & (addseq f) . (a,b) = xj + yj ) by defadd;
x + y = xj + yj by AS, A, lem2;
hence a + b = x + y by A, dsf; :: thesis: a * b = x * y
consider j being Element of NAT , xj, yj being Element of (f . j) such that
A: ( xj = a & yj = b & (multseq f) . (a,b) = xj * yj ) by H, defmult;
x * y = xj * yj by AS, A, lem2;
hence a * b = x * y by A, dsf; :: thesis: verum