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); :: thesis: ( ( 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) ) ) ; :: thesis: g1 = g2
for x being Element of (FlatPoset X) holds g1 . x = g2 . x

proof

let x be Element of (FlatPoset X); :: thesis: g1 . x = g2 . x
g1 . x = BaseFunc01 (x,(h . ((Flatten E) . x)),I,J,D) by B1
.= g2 . x by B1 ;
hence g1 . x = g2 . x ; :: thesis: verum

end;

hence g1 = g2 ; :: thesis: verum

end;

hence for b₁, b₂ 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
b₁ . 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
b₂ . x = BaseFunc01 (x,(f . ((Flatten E) . x)),I,J,D) ) holds
b₁ = b₂ ; :: thesis: verum