let Seq1, Seq2 be Covering of union (rng Sets),F; :: thesis: ( ( for n being Nat holds Seq1 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) ) & ( for n being Nat holds Seq2 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) ) implies Seq1 = Seq2 )
assume that
A11: for n being Nat holds Seq1 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) and
A12: for n being Nat holds Seq2 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) ; :: thesis: Seq1 = Seq2
for n being object st n in NAT holds
Seq1 . n = Seq2 . n
proof
let n be object ; :: thesis: ( n in NAT implies Seq1 . n = Seq2 . n )
assume n in NAT ; :: thesis: Seq1 . n = Seq2 . n
then reconsider n = n as Element of NAT ;
Seq1 . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) by A11;
hence Seq1 . n = Seq2 . n by A12; :: thesis: verum
end;
hence Seq1 = Seq2 by FUNCT_2:12; :: thesis: verum