set FX = FlatPoset X;
set CX = succ X;
set FY = FlatPoset Y;
set CY = succ Y;
reconsider h1 = h1, h2 = h2 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 f1, f2 being continuous Function of (FlatPoset X),(FlatPoset Y) st h1 = f1 & h2 = f2 holds
g1 . x = BaseFunc02 (x,(f1 . ((Flatten E1) . x)),(f2 . ((Flatten E2) . x)),I,J,D) ) & ( for x being Element of (FlatPoset X)
for f1, f2 being continuous Function of (FlatPoset X),(FlatPoset Y) st h1 = f1 & h2 = f2 holds
g2 . x = BaseFunc02 (x,(f1 . ((Flatten E1) . x)),(f2 . ((Flatten E2) . 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 f1, f2 being continuous Function of (FlatPoset X),(FlatPoset Y) st h1 = f1 & h2 = f2 holds
g1 . x = BaseFunc02 (x,(f1 . ((Flatten E1) . x)),(f2 . ((Flatten E2) . x)),I,J,D) ) & ( for x being Element of (FlatPoset X)
for f1, f2 being continuous Function of (FlatPoset X),(FlatPoset Y) st h1 = f1 & h2 = f2 holds
g2 . x = BaseFunc02 (x,(f1 . ((Flatten E1) . x)),(f2 . ((Flatten E2) . x)),I,J,D) ) implies g1 = g2 )
assume B1: ( ( for x being Element of (FlatPoset X)
for f1, f2 being continuous Function of (FlatPoset X),(FlatPoset Y) st h1 = f1 & h2 = f2 holds
g1 . x = BaseFunc02 (x,(f1 . ((Flatten E1) . x)),(f2 . ((Flatten E2) . x)),I,J,D) ) & ( for x being Element of (FlatPoset X)
for f1, f2 being continuous Function of (FlatPoset X),(FlatPoset Y) st h1 = f1 & h2 = f2 holds
g2 . x = BaseFunc02 (x,(f1 . ((Flatten E1) . x)),(f2 . ((Flatten E2) . 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 = BaseFunc02 (x,(h1 . ((Flatten E1) . x)),(h2 . ((Flatten E2) . 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 b1, b2 being continuous Function of (FlatPoset X),(FlatPoset Y) st ( for x being Element of (FlatPoset X)
for f1, f2 being continuous Function of (FlatPoset X),(FlatPoset Y) st h1 = f1 & h2 = f2 holds
b1 . x = BaseFunc02 (x,(f1 . ((Flatten E1) . x)),(f2 . ((Flatten E2) . x)),I,J,D) ) & ( for x being Element of (FlatPoset X)
for f1, f2 being continuous Function of (FlatPoset X),(FlatPoset Y) st h1 = f1 & h2 = f2 holds
b2 . x = BaseFunc02 (x,(f1 . ((Flatten E1) . x)),(f2 . ((Flatten E2) . x)),I,J,D) ) holds
b1 = b2 ; :: thesis: verum