let G1, G2 be Interval_Covering of union (rng F); :: thesis: ( ( for n being Element of NAT holds G1 . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) ) & ( for n being Element of NAT holds G2 . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) ) implies G1 = G2 )
assume that
A16: for n being Element of NAT holds G1 . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) and
A17: for n being Element of NAT holds G2 . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) ; :: thesis: G1 = G2
for n being object st n in NAT holds
G1 . n = G2 . n
proof
let n be object ; :: thesis: ( n in NAT implies G1 . n = G2 . n )
assume n in NAT ; :: thesis: G1 . n = G2 . n
then reconsider n = n as Element of NAT ;
G1 . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) by A16;
hence G1 . n = G2 . n by A17; :: thesis: verum
end;
hence G1 = G2 by FUNCT_2:12; :: thesis: verum