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:
A2: ( not X in X & not Y in Y ) ;
set FX = FlatPoset X;
set CX = succ X;
set FY = FlatPoset Y;
set CY = succ Y;
consider f, g being set such that
A7: ( f in ConFuncs ((FlatPoset X),(FlatPoset Y)) & g in ConFuncs ((FlatPoset X),(FlatPoset Y)) & f = RecFunc02 (f,g,E1,E2,I1,J1,D) & g = RecFunc02 (f,g,E1,E2,I2,J2,D) ) by Threcursive0201;
reconsider f = f, g = g as continuous Function of (FlatPoset X),(FlatPoset Y) by A7;
take f ; :: thesis:
take g ; :: thesis:
consider l being Function of X,NAT such that
A801: for x0 being Element of X holds
( ( l . x0 <= 0 implies x0 in D ) & ( not x0 in D implies ( l . (E1 . x0) < l . x0 & l . (E2 . x0) < l . x0 ) ) ) by A1;
defpred S₁[ Nat] means for x1, x2 being Element of X st l . x1 <= $1 & l . x2 <= $1 holds
( f . x1 in Y & f . x1 = BaseFunc02 (x1,(f . (E1 . x1)),(g . (E2 . x1)),I1,J1,D) & g . x2 in Y & g . x2 = BaseFunc02 (x2,(f . (E1 . x2)),(g . (E2 . x2)),I2,J2,D) );
A9: S₁[ 0 ]

let x1, x2 be Element of X; :: thesis:
assume b1: ( l . x1 <= 0 & l . x2 <= 0 ) ; :: thesis:
B2: ( x1 in X & x2 in X ) ;
reconsider x1 = x1, x2 = x2 as Element of (FlatPoset X) by XBOOLE_0:def 3;
( x1 <> X & x2 <> X ) by B2;
then B4: ( f . ((Flatten E1) . x1) = f . (E1 . x1) & g . ((Flatten E2) . x1) = g . (E2 . x1) & f . ((Flatten E1) . x2) = f . (E1 . x2) & g . ((Flatten E2) . x2) = g . (E2 . x2) ) by DefFlatten04;
f . x1 = BaseFunc02 (x1,(f . (E1 . x1)),(g . (E2 . x1)),I1,J1,D) by A7, DefRecFunc02, B4;
then B6: f . x1 = I1 . x1 by DefBaseFunc02, b1, A801;
g . x2 = BaseFunc02 (x2,(f . (E1 . x2)),(g . (E2 . x2)),I2,J2,D) by A7, DefRecFunc02, B4;
then g . x2 = I2 . x2 by DefBaseFunc02, b1, A801;
hence ( f . x1 in Y & f . x1 = BaseFunc02 (x1,(f . (E1 . x1)),(g . (E2 . x1)),I1,J1,D) & g . x2 in Y & g . x2 = BaseFunc02 (x2,(f . (E1 . x2)),(g . (E2 . x2)),I2,J2,D) ) by A7, DefRecFunc02, B4, FUNCT_2:5, B6; :: thesis:

end;

A10: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis:
assume B0: S₁[k] ; :: thesis:
let x01, x02 be Element of X; :: thesis:
assume B1: ( l . x01 <= k + 1 & l . x02 <= k + 1 ) ; :: thesis:
reconsider x01 = x01, x02 = x02 as Element of (FlatPoset X) by XBOOLE_0:def 3;
( x01 <> X & x02 <> X ) by A2;
then B4: ( f . ((Flatten E1) . x01) = f . (E1 . x01) & g . ((Flatten E2) . x01) = g . (E2 . x01) & f . ((Flatten E1) . x02) = f . (E1 . x02) & g . ((Flatten E2) . x02) = g . (E2 . x02) ) by DefFlatten04;
set x11 = E1 . x01;
set x21 = E2 . x01;
set x12 = E1 . x02;
set x22 = E2 . x02;
reconsider x11 = E1 . x01, x12 = E1 . x02, x21 = E2 . x01, x22 = E2 . x02 as Element of X by FUNCT_2:5;
B501: f . x01 = BaseFunc02 (x01,(f . x11),(g . x21),I1,J1,D) by A7, DefRecFunc02, B4;
B502: g . x02 = BaseFunc02 (x02,(f . x12),(g . x22),I2,J2,D) by A7, DefRecFunc02, B4;
reconsider x01 = x01, x02 = x02 as Element of X ;

then g . x02 = I2 . x02 by DefBaseFunc02, B502;
hence ( f . x01 in Y & f . x01 = BaseFunc02 (x01,(f . (E1 . x01)),(g . (E2 . x01)),I1,J1,D) & g . x02 in Y & g . x02 = BaseFunc02 (x02,(f . (E1 . x02)),(g . (E2 . x02)),I2,J2,D) ) by C2, A7, DefRecFunc02, B4; :: thesis:

end;

then ( (l . x12) + 1 <= l . x02 & (l . x22) + 1 <= l . x02 ) by NAT_1:13, A801;
then ( (l . x12) + 1 <= k + 1 & (l . x22) + 1 <= k + 1 ) by B1, XXREAL_0:2;
then ( l . x12 <= k & l . x22 <= k ) by XREAL_1:8;
then C04: ( f . x12 in Y & g . x22 in Y ) by B0;
C06: g . x02 = J2 . [x02,(f . x12),(g . x22)] by B502, DefBaseFunc02, C01, C04;
[x02,(f . x12),(g . x22)] in [:X,Y,Y:] by C04, MCART_1:69;
hence ( f . x01 in Y & f . x01 = BaseFunc02 (x01,(f . (E1 . x01)),(g . (E2 . x01)),I1,J1,D) & g . x02 in Y & g . x02 = BaseFunc02 (x02,(f . (E1 . x02)),(g . (E2 . x02)),I2,J2,D) ) by C2, C06, A7, DefRecFunc02, B4, FUNCT_2:5; :: thesis:

end;

then ( (l . x11) + 1 <= l . x01 & (l . x21) + 1 <= l . x01 ) by NAT_1:13, A801;
then ( (l . x11) + 1 <= k + 1 & (l . x21) + 1 <= k + 1 ) by B1, XXREAL_0:2;
then ( l . x11 <= k & l . x21 <= k ) by XREAL_1:8;
then C4: ( f . x11 in Y & g . x21 in Y ) by B0;
then C6: f . x01 = J1 . [x01,(f . x11),(g . x21)] by B501, DefBaseFunc02, C1;
C7: [x01,(f . x11),(g . x21)] in [:X,Y,Y:] by C4, MCART_1:69;

end;

then ( (l . x12) + 1 <= l . x02 & (l . x22) + 1 <= l . x02 ) by NAT_1:13, A801;
then ( (l . x12) + 1 <= k + 1 & (l . x22) + 1 <= k + 1 ) by B1, XXREAL_0:2;
then ( l . x12 <= k & l . x22 <= k ) by XREAL_1:8;
then C04: ( f . x12 in Y & g . x22 in Y ) by B0;
C06: g . x02 = J2 . [x02,(f . x12),(g . x22)] by B502, DefBaseFunc02, C01, C04;
[x02,(f . x12),(g . x22)] in [:X,Y,Y:] by C04, MCART_1:69;
hence ( f . x01 in Y & f . x01 = BaseFunc02 (x01,(f . (E1 . x01)),(g . (E2 . x01)),I1,J1,D) & g . x02 in Y & g . x02 = BaseFunc02 (x02,(f . (E1 . x02)),(g . (E2 . x02)),I2,J2,D) ) by C6, C7, C06, A7, DefRecFunc02, B4, FUNCT_2:5; :: thesis:

end;

A11: for k being Nat holds S₁[k] from NAT_1:sch 2(A9, A10);
for x1, x2 being Element of X holds
( f . x1 in Y & f . x1 = BaseFunc02 (x1,(f . (E1 . x1)),(g . (E2 . x1)),I1,J1,D) & g . x2 in Y & g . x2 = BaseFunc02 (x2,(f . (E1 . x2)),(g . (E2 . x2)),I2,J2,D) )

let x1, x2 be Element of X; :: thesis:
reconsider k = (l . x1) + (l . x2) as Nat ;
( l . x1 <= k & l . x2 <= k ) by NAT_1:11;
hence ( f . x1 in Y & f . x1 = BaseFunc02 (x1,(f . (E1 . x1)),(g . (E2 . x1)),I1,J1,D) & g . x2 in Y & g . x2 = BaseFunc02 (x2,(f . (E1 . x2)),(g . (E2 . x2)),I2,J2,D) ) by A11; :: thesis:

end;

hence 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) ) ; :: thesis: