let x, y be set ; :: thesis: ( ex f being Sequence st
( alpha in dom f & f . alpha = x & ( for beta being Ordinal st beta in dom f holds
f . beta = { left-right(# x,y #) where x, y is Subset of (union (rng (f | beta))) : verum } ) ) & ex f being Sequence st
( alpha in dom f & f . alpha = y & ( for beta being Ordinal st beta in dom f holds
f . beta = { left-right(# x,y #) where x, y is Subset of (union (rng (f | beta))) : verum } ) ) implies x = y )
assume ex f1 being Sequence st
( alpha in dom f1 & f1 . alpha = x & S1[f1] ) ; :: thesis: ( for f being Sequence holds
( not alpha in dom f or not f . alpha = y or ex beta being Ordinal st
( beta in dom f & not f . beta = { left-right(# x,y #) where x, y is Subset of (union (rng (f | beta))) : verum } ) ) or x = y )
then consider f1 being Sequence such that
A2: ( alpha in dom f1 & f1 . alpha = x & S1[f1] ) ;
set f1r = f1 | (succ alpha);
assume ex f2 being Sequence st
( alpha in dom f2 & f2 . alpha = y & S1[f2] ) ; :: thesis: x = y
then consider f2 being Sequence such that
A3: ( alpha in dom f2 & f2 . alpha = y & S1[f2] ) ;
set f2r = f2 | (succ alpha);
A4: ( dom (f1 | (succ alpha)) = succ alpha & ( for beta being Ordinal
for f being Sequence st beta in succ alpha & f = (f1 | (succ alpha)) | beta holds
(f1 | (succ alpha)) . beta = H1(f) ) )
proof
succ alpha c= dom f1 by A2, ORDINAL1:21;
hence A5: dom (f1 | (succ alpha)) = succ alpha by RELAT_1:62; :: thesis: for beta being Ordinal
for f being Sequence st beta in succ alpha & f = (f1 | (succ alpha)) | beta holds
(f1 | (succ alpha)) . beta = H1(f)
let beta be Ordinal; :: thesis: for f being Sequence st beta in succ alpha & f = (f1 | (succ alpha)) | beta holds
(f1 | (succ alpha)) . beta = H1(f)
let f be Sequence; :: thesis: ( beta in succ alpha & f = (f1 | (succ alpha)) | beta implies (f1 | (succ alpha)) . beta = H1(f) )
assume ( beta in succ alpha & f = (f1 | (succ alpha)) | beta ) ; :: thesis: (f1 | (succ alpha)) . beta = H1(f)
hence (f1 | (succ alpha)) . beta = H1(f) by A5, Lm1, A2; :: thesis: verum
end;
A6: ( dom (f2 | (succ alpha)) = succ alpha & ( for beta being Ordinal
for f being Sequence st beta in succ alpha & f = (f2 | (succ alpha)) | beta holds
(f2 | (succ alpha)) . beta = H1(f) ) )
proof
succ alpha c= dom f2 by A3, ORDINAL1:21;
hence A7: dom (f2 | (succ alpha)) = succ alpha by RELAT_1:62; :: thesis: for beta being Ordinal
for f being Sequence st beta in succ alpha & f = (f2 | (succ alpha)) | beta holds
(f2 | (succ alpha)) . beta = H1(f)
let beta be Ordinal; :: thesis: for f being Sequence st beta in succ alpha & f = (f2 | (succ alpha)) | beta holds
(f2 | (succ alpha)) . beta = H1(f)
let f be Sequence; :: thesis: ( beta in succ alpha & f = (f2 | (succ alpha)) | beta implies (f2 | (succ alpha)) . beta = H1(f) )
assume ( beta in succ alpha & f = (f2 | (succ alpha)) | beta ) ; :: thesis: (f2 | (succ alpha)) . beta = H1(f)
hence (f2 | (succ alpha)) . beta = H1(f) by A7, Lm1, A3; :: thesis: verum
end;
A8: ( (f1 | (succ alpha)) . alpha = f1 . alpha & (f2 | (succ alpha)) . alpha = f2 . alpha ) by FUNCT_1:49, ORDINAL1:6;
f1 | (succ alpha) = f2 | (succ alpha) from ORDINAL1:sch 3(A4, A6);
 hence x = y by A2, A3, A8; :: thesis: verum