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;

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

hence
seq1 = seq2
by A4, FUNCT_1:2, PARTFUN1:def 2; :: thesis: verumseq1 . 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;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