let X, Y be non empty set ; :: thesis:
let D be Subset of X; :: thesis:
let I be Function of X,Y; :: thesis:
let J be Function of [:X,Y:],Y; :: thesis:
let E be Function of X,X; :: thesis:
let f1, f2 be Function of X,Y; :: thesis:
assume A0: ( E is_well_founded_with_minimal_set D & ( for x being Element of X holds
( ( x in D implies f1 . x = I . x ) & ( not x in D implies f1 . x = J . [x,(f1 . (E . x))] ) ) ) & ( for x being Element of X holds
( ( x in D implies f2 . x = I . x ) & ( not x in D implies f2 . x = J . [x,(f2 . (E . x))] ) ) ) ) ; :: thesis:
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 . (E . x) < l . x ) ) ;
defpred S₁[ Nat] means for x being Element of X st l . x <= $1 holds
f1 . x = f2 . x;
A2: S₁[ 0 ]

let x be Element of X; :: thesis:
assume b1: l . x <= 0 ; :: thesis:
then f1 . x = I . x by A0, A1
.= f2 . x by A0, b1, A1 ;
hence f1 . x = f2 . x ; :: thesis:

end;

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

f1 . x = I . x by A0, C0
.= f2 . x by A0, C0 ;
hence f1 . x = f2 . x ; :: thesis:

end;

reconsider x1 = E . x as Element of X ;
reconsider x = x as Element of X ;
(l . x1) + 1 <= l . x by NAT_1:13, A1, C0;
then c2: (l . x1) + 1 <= k + 1 by B1, XXREAL_0:2;
f1 . x = J . [x,(f1 . x1)] by A0, C0
.= J . [x,(f2 . x1)] by c2, B0, XREAL_1:8
.= f2 . x by A0, C0 ;
hence f1 . x = f2 . x ; :: thesis:

end;

let x be Element of X; :: thesis:
reconsider k = l . x as Nat ;
l . x <= k ;
hence f1 . x = f2 . x by A4; :: thesis:

end;

hence f1 = f2 ; :: thesis: