let X, Y be non empty set ; :: thesis:
let D be Subset of X; :: thesis:
let I1, I2 be Function of X,Y; :: thesis:
let J1, J2 be Function of [:X,Y,Y:],Y; :: thesis:
let E1, E2 be Function of X,X; :: thesis:
assume A1: E1,E2 is_well_founded_with_minimal_set D ; :: thesis:
set FX = FlatPoset X;
set CX = succ X;
A02: X c= succ X by XBOOLE_1:7;
set FY = FlatPoset Y;
set CY = succ Y;
consider f, g being continuous Function of (FlatPoset X),(FlatPoset Y) such that
A3: for x being Element of X holds
( f . x in Y & f . x = BaseFunc02 (x,(f . (E1 . x)),(g . (E2 . x)),I1,J1,D) & g . x in Y & g . x = BaseFunc02 (x,(f . (E1 . x)),(g . (E2 . x)),I2,J2,D) ) by A1, Threcursive0301;
reconsider f = f, g = g as Function of (succ X),(succ Y) ;
reconsider fX = f | X, gX = g | X as Function of X,(succ Y) by A02, FUNCT_2:32;
for x being Element of X holds
( fX . x in Y & gX . x in Y )

let x be Element of X; :: thesis:
( f . x in Y & g . x in Y ) by A3;
hence ( fX . x in Y & gX . x in Y ) by FUNCT_1:49; :: thesis:

end;

then ( rng fX c= Y & rng gX c= Y ) by FUNCT_2:114;
then reconsider fX = fX, gX = gX as Function of X,Y by FUNCT_2:6;
take fX ; :: thesis:
take gX ; :: thesis:
let x be Element of X; :: thesis:
reconsider x1 = E1 . x, x2 = E2 . x as Element of X ;
B2: ( fX . x1 = f . x1 & gX . x2 = g . x2 ) by FUNCT_1:49;
B3: fX . x = f . x by FUNCT_1:49
.= BaseFunc02 (x,(fX . x1),(gX . x2),I1,J1,D) by A3, B2 ;
gX . x = g . x by FUNCT_1:49
.= BaseFunc02 (x,(f . x1),(g . x2),I2,J2,D) by A3 ;
hence ( fX . x = BaseFunc02 (x,(fX . (E1 . x)),(gX . (E2 . x)),I1,J1,D) & gX . x = BaseFunc02 (x,(fX . (E1 . x)),(gX . (E2 . x)),I2,J2,D) ) by B2, B3; :: thesis: