let seq1, seq2 be SigmaField_sequence of D; :: thesis: ( ( for n being Nat holds seq1 . n = Trivial-SigmaField (D . n) ) & ( for n being Nat holds seq2 . n = Trivial-SigmaField (D . n) ) implies seq1 = seq2 )
assume that
A2: for n being Nat holds seq1 . n = Trivial-SigmaField (D . n) and
A3: for n being Nat holds seq2 . n = Trivial-SigmaField (D . n) ; :: thesis: seq1 = seq2
A4: dom seq2 = NAT by PARTFUN1:def 2;

now :: thesis: for n being object st n in dom seq1 holds
seq1 . n = seq2 . n

let n be object ; :: thesis: ( n in dom seq1 implies seq1 . n = seq2 . n )
assume n in dom seq1 ; :: thesis: seq1 . n = seq2 . n
then reconsider i = n as Nat ;
thus seq1 . n = Trivial-SigmaField (D . i) by A2
.= seq2 . n by A3 ; :: thesis: verum

end;

hence seq1 = seq2 by A4, FUNCT_1:2, PARTFUN1:def 2; :: thesis: verum