let S1, S2 be SetSequence of REAL; ( S1 . 0 = Union (GoCross_Partial_Union (pm,0)) & ( for n being Nat holds S1 . (n + 1) = (S1 . n) \/ (Union (GoCross_Partial_Union (pm,(n + 1)))) ) & S2 . 0 = Union (GoCross_Partial_Union (pm,0)) & ( for n being Nat holds S2 . (n + 1) = (S2 . n) \/ (Union (GoCross_Partial_Union (pm,(n + 1)))) ) implies S1 = S2 )
assume that
A4:
S1 . 0 = Union (GoCross_Partial_Union (pm,0))
and
A5:
for n being Nat holds S1 . (n + 1) = (S1 . n) \/ (Union (GoCross_Partial_Union (pm,(n + 1))))
and
A6:
S2 . 0 = Union (GoCross_Partial_Union (pm,0))
and
A7:
for n being Nat holds S2 . (n + 1) = (S2 . n) \/ (Union (GoCross_Partial_Union (pm,(n + 1))))
; S1 = S2
defpred S1[ object ] means S1 . $1 = S2 . $1;
for n being object st n in NAT holds
S1[n]
proof
let n be
object ;
( n in NAT implies S1[n] )
assume
n in NAT
;
S1[n]
then reconsider n =
n as
Nat ;
A8:
for
k2 being
Nat st
S1[
k2] holds
S1[
k2 + 1]
A9:
S1[
0 ]
by A4, A6;
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A9, A8);
then
S1 . n = S2 . n
;
hence
S1[
n]
;
verum
end;
hence
S1 = S2
; verum