let X, Y be non empty set ; :: thesis: for D being Subset of X
for I1, I2 being Function of X,Y
for J1, J2 being Function of [:X,Y,Y:],Y
for E1, E2 being Function of X,X
for f1, g1, f2, g2 being Function of X,Y st E1,E2 is_well_founded_with_minimal_set D & ( for x being Element of X holds
( ( x in D implies ( f1 . x = I1 . x & g1 . x = I2 . x ) ) & ( not x in D implies ( f1 . x = J1 . [x,(f1 . (E1 . x)),(g1 . (E2 . x))] & g1 . x = J2 . [x,(f1 . (E1 . x)),(g1 . (E2 . x))] ) ) ) ) & ( for x being Element of X holds
( ( x in D implies ( f2 . x = I1 . x & g2 . x = I2 . x ) ) & ( not x in D implies ( f2 . x = J1 . [x,(f2 . (E1 . x)),(g2 . (E2 . x))] & g2 . x = J2 . [x,(f2 . (E1 . x)),(g2 . (E2 . x))] ) ) ) ) holds
( f1 = f2 & g1 = g2 )
let D be Subset of X; :: thesis: for I1, I2 being Function of X,Y
for J1, J2 being Function of [:X,Y,Y:],Y
for E1, E2 being Function of X,X
for f1, g1, f2, g2 being Function of X,Y st E1,E2 is_well_founded_with_minimal_set D & ( for x being Element of X holds
( ( x in D implies ( f1 . x = I1 . x & g1 . x = I2 . x ) ) & ( not x in D implies ( f1 . x = J1 . [x,(f1 . (E1 . x)),(g1 . (E2 . x))] & g1 . x = J2 . [x,(f1 . (E1 . x)),(g1 . (E2 . x))] ) ) ) ) & ( for x being Element of X holds
( ( x in D implies ( f2 . x = I1 . x & g2 . x = I2 . x ) ) & ( not x in D implies ( f2 . x = J1 . [x,(f2 . (E1 . x)),(g2 . (E2 . x))] & g2 . x = J2 . [x,(f2 . (E1 . x)),(g2 . (E2 . x))] ) ) ) ) holds
( f1 = f2 & g1 = g2 )
let I1, I2 be Function of X,Y; :: thesis: for J1, J2 being Function of [:X,Y,Y:],Y
for E1, E2 being Function of X,X
for f1, g1, f2, g2 being Function of X,Y st E1,E2 is_well_founded_with_minimal_set D & ( for x being Element of X holds
( ( x in D implies ( f1 . x = I1 . x & g1 . x = I2 . x ) ) & ( not x in D implies ( f1 . x = J1 . [x,(f1 . (E1 . x)),(g1 . (E2 . x))] & g1 . x = J2 . [x,(f1 . (E1 . x)),(g1 . (E2 . x))] ) ) ) ) & ( for x being Element of X holds
( ( x in D implies ( f2 . x = I1 . x & g2 . x = I2 . x ) ) & ( not x in D implies ( f2 . x = J1 . [x,(f2 . (E1 . x)),(g2 . (E2 . x))] & g2 . x = J2 . [x,(f2 . (E1 . x)),(g2 . (E2 . x))] ) ) ) ) holds
( f1 = f2 & g1 = g2 )
let J1, J2 be Function of [:X,Y,Y:],Y; :: thesis: for E1, E2 being Function of X,X
for f1, g1, f2, g2 being Function of X,Y st E1,E2 is_well_founded_with_minimal_set D & ( for x being Element of X holds
( ( x in D implies ( f1 . x = I1 . x & g1 . x = I2 . x ) ) & ( not x in D implies ( f1 . x = J1 . [x,(f1 . (E1 . x)),(g1 . (E2 . x))] & g1 . x = J2 . [x,(f1 . (E1 . x)),(g1 . (E2 . x))] ) ) ) ) & ( for x being Element of X holds
( ( x in D implies ( f2 . x = I1 . x & g2 . x = I2 . x ) ) & ( not x in D implies ( f2 . x = J1 . [x,(f2 . (E1 . x)),(g2 . (E2 . x))] & g2 . x = J2 . [x,(f2 . (E1 . x)),(g2 . (E2 . x))] ) ) ) ) holds
( f1 = f2 & g1 = g2 )
let E1, E2 be Function of X,X; :: thesis: for f1, g1, f2, g2 being Function of X,Y st E1,E2 is_well_founded_with_minimal_set D & ( for x being Element of X holds
( ( x in D implies ( f1 . x = I1 . x & g1 . x = I2 . x ) ) & ( not x in D implies ( f1 . x = J1 . [x,(f1 . (E1 . x)),(g1 . (E2 . x))] & g1 . x = J2 . [x,(f1 . (E1 . x)),(g1 . (E2 . x))] ) ) ) ) & ( for x being Element of X holds
( ( x in D implies ( f2 . x = I1 . x & g2 . x = I2 . x ) ) & ( not x in D implies ( f2 . x = J1 . [x,(f2 . (E1 . x)),(g2 . (E2 . x))] & g2 . x = J2 . [x,(f2 . (E1 . x)),(g2 . (E2 . x))] ) ) ) ) holds
( f1 = f2 & g1 = g2 )
let f1, g1, f2, g2 be Function of X,Y; :: thesis: ( E1,E2 is_well_founded_with_minimal_set D & ( for x being Element of X holds
( ( x in D implies ( f1 . x = I1 . x & g1 . x = I2 . x ) ) & ( not x in D implies ( f1 . x = J1 . [x,(f1 . (E1 . x)),(g1 . (E2 . x))] & g1 . x = J2 . [x,(f1 . (E1 . x)),(g1 . (E2 . x))] ) ) ) ) & ( for x being Element of X holds
( ( x in D implies ( f2 . x = I1 . x & g2 . x = I2 . x ) ) & ( not x in D implies ( f2 . x = J1 . [x,(f2 . (E1 . x)),(g2 . (E2 . x))] & g2 . x = J2 . [x,(f2 . (E1 . x)),(g2 . (E2 . x))] ) ) ) ) implies ( f1 = f2 & g1 = g2 ) )
assume A0: ( E1,E2 is_well_founded_with_minimal_set D & ( for x being Element of X holds
( ( x in D implies ( f1 . x = I1 . x & g1 . x = I2 . x ) ) & ( not x in D implies ( f1 . x = J1 . [x,(f1 . (E1 . x)),(g1 . (E2 . x))] & g1 . x = J2 . [x,(f1 . (E1 . x)),(g1 . (E2 . x))] ) ) ) ) & ( for x being Element of X holds
( ( x in D implies ( f2 . x = I1 . x & g2 . x = I2 . x ) ) & ( not x in D implies ( f2 . x = J1 . [x,(f2 . (E1 . x)),(g2 . (E2 . x))] & g2 . x = J2 . [x,(f2 . (E1 . x)),(g2 . (E2 . x))] ) ) ) ) ) ; :: thesis: ( f1 = f2 & g1 = g2 )
then consider l being Function of X,NAT such that
A1: for x being Element of X holds
( ( l . x <= 0 implies x in D ) & ( not x in D implies ( l . (E1 . x) < l . x & l . (E2 . x) < l . x ) ) ) ;
defpred S1[ Nat] means for x being Element of X st l . x <= $1 holds
( f1 . x = f2 . x & g1 . x = g2 . x );
A2: S1[ 0 ]
proof
let x be Element of X; :: thesis: ( l . x <= 0 implies ( f1 . x = f2 . x & g1 . x = g2 . x ) )
assume l . x <= 0 ; :: thesis: ( f1 . x = f2 . x & g1 . x = g2 . x )
then B1: x in D by A1;
B2: f1 . x = I1 . x by A0, B1
.= f2 . x by A0, B1 ;
g1 . x = I2 . x by A0, B1
.= g2 . x by A0, B1 ;
hence ( f1 . x = f2 . x & g1 . x = g2 . x ) by B2; :: thesis: verum
end;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume B0: S1[k] ; :: thesis: S1[k + 1]
let x be Element of X; :: thesis: ( l . x <= k + 1 implies ( f1 . x = f2 . x & g1 . x = g2 . x ) )
assume B1: l . x <= k + 1 ; :: thesis: ( f1 . x = f2 . x & g1 . x = g2 . x )
per cases ( x in D or not x in D ) ;
suppose C0: x in D ; :: thesis: ( f1 . x = f2 . x & g1 . x = g2 . x )
C1: f1 . x = I1 . x by A0, C0
.= f2 . x by A0, C0 ;
g1 . x = I2 . x by A0, C0
.= g2 . x by A0, C0 ;
hence ( f1 . x = f2 . x & g1 . x = g2 . x ) by C1; :: thesis: verum
end;
suppose C0: not x in D ; :: thesis: ( f1 . x = f2 . x & g1 . x = g2 . x )
reconsider x1 = E1 . x, x2 = E2 . x as Element of X ;
( (l . x1) + 1 <= l . x & (l . x2) + 1 <= l . x ) by NAT_1:13, A1, C0;
then ( (l . x1) + 1 <= k + 1 & (l . x2) + 1 <= k + 1 ) by B1, XXREAL_0:2;
then ( l . x1 <= k & l . x2 <= k ) by XREAL_1:8;
then C1: ( f1 . x1 = f2 . x1 & g1 . x2 = g2 . x2 ) by B0;
C2: f1 . x = J1 . [x,(f2 . x1),(g2 . x2)] by A0, C0, C1
.= f2 . x by A0, C0 ;
g1 . x = J2 . [x,(f2 . x1),(g2 . x2)] by A0, C0, C1
.= g2 . x by A0, C0 ;
hence ( f1 . x = f2 . x & g1 . x = g2 . x ) by C2; :: thesis: verum
end;
end;
end;
A4: for k being Nat holds S1[k] from NAT_1:sch 2(A2, A3);
 for x being Element of X holds
( f1 . x = f2 . x & g1 . x = g2 . x )
proof
let x be Element of X; :: thesis: ( f1 . x = f2 . x & g1 . x = g2 . x )
reconsider k = l . x as Nat ;
l . x <= k ;
hence ( f1 . x = f2 . x & g1 . x = g2 . x ) by A4; :: thesis: verum
end;
hence ( f1 = f2 & g1 = g2 ) ; :: thesis: verum