set FX = FlatPoset X;
set CX = succ X;
set FY = FlatPoset Y;
set CY = succ Y;
reconsider h = h as continuous Function of (FlatPoset X),(FlatPoset Y) by A00;
for g1, g2 being continuous Function of (FlatPoset X),(FlatPoset Y) st ( for x being Element of (FlatPoset X)
for f being continuous Function of (FlatPoset X),(FlatPoset Y) st h = f holds
g1 . x = BaseFunc01 (x,(f . ((Flatten E) . x)),I,J,D) ) & ( for x being Element of (FlatPoset X)
for f being continuous Function of (FlatPoset X),(FlatPoset Y) st h = f holds
g2 . x = BaseFunc01 (x,(f . ((Flatten E) . x)),I,J,D) ) holds
g1 = g2
proof
let g1,
g2 be
continuous Function of
(FlatPoset X),
(FlatPoset Y);
( ( for x being Element of (FlatPoset X)
for f being continuous Function of (FlatPoset X),(FlatPoset Y) st h = f holds
g1 . x = BaseFunc01 (x,(f . ((Flatten E) . x)),I,J,D) ) & ( for x being Element of (FlatPoset X)
for f being continuous Function of (FlatPoset X),(FlatPoset Y) st h = f holds
g2 . x = BaseFunc01 (x,(f . ((Flatten E) . x)),I,J,D) ) implies g1 = g2 )
assume B1:
( ( for
x being
Element of
(FlatPoset X) for
f being
continuous Function of
(FlatPoset X),
(FlatPoset Y) st
h = f holds
g1 . x = BaseFunc01 (
x,
(f . ((Flatten E) . x)),
I,
J,
D) ) & ( for
x being
Element of
(FlatPoset X) for
f being
continuous Function of
(FlatPoset X),
(FlatPoset Y) st
h = f holds
g2 . x = BaseFunc01 (
x,
(f . ((Flatten E) . x)),
I,
J,
D) ) )
;
g1 = g2
for
x being
Element of
(FlatPoset X) holds
g1 . x = g2 . x
hence
g1 = g2
;
verum
end;
hence
for b1, b2 being continuous Function of (FlatPoset X),(FlatPoset Y) st ( for x being Element of (FlatPoset X)
for f being continuous Function of (FlatPoset X),(FlatPoset Y) st h = f holds
b1 . x = BaseFunc01 (x,(f . ((Flatten E) . x)),I,J,D) ) & ( for x being Element of (FlatPoset X)
for f being continuous Function of (FlatPoset X),(FlatPoset Y) st h = f holds
b2 . x = BaseFunc01 (x,(f . ((Flatten E) . x)),I,J,D) ) holds
b1 = b2
; verum