let X, Y be non empty set ; :: thesis: for D being Subset of X
for I being Function of X,Y
for J being Function of [:X,Y:],Y
for E being Function of X,X
for f1, f2 being Function of X,Y st 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))] ) ) ) holds
f1 = f2
let D be Subset of X; :: thesis: for I being Function of X,Y
for J being Function of [:X,Y:],Y
for E being Function of X,X
for f1, f2 being Function of X,Y st 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))] ) ) ) holds
f1 = f2
let I be Function of X,Y; :: thesis: for J being Function of [:X,Y:],Y
for E being Function of X,X
for f1, f2 being Function of X,Y st 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))] ) ) ) holds
f1 = f2
let J be Function of [:X,Y:],Y; :: thesis: for E being Function of X,X
for f1, f2 being Function of X,Y st 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))] ) ) ) holds
f1 = f2
let E be Function of X,X; :: thesis: for f1, f2 being Function of X,Y st 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))] ) ) ) holds
f1 = f2
let f1, f2 be Function of X,Y; :: thesis: ( 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))] ) ) ) implies f1 = f2 )
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: f1 = f2
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 ]

proof

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

end;

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

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume B0: S₁[k] ; :: thesis: S₁[k + 1]
let x be Element of X; :: thesis: ( l . x <= k + 1 implies f1 . x = f2 . x )
assume B1: l . x <= k + 1 ; :: thesis: f1 . x = f2 . x

per cases ( x in D or not x in D ) ;

suppose C0: x in D ; :: thesis: f1 . x = f2 . x

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

end;

suppose C0: not x in D ; :: thesis: f1 . x = f2 . x

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: verum

end;

end;

end;

A4: for k being Nat holds S₁[k] from NAT_1:sch 2(A2, A3);
for x being Element of X holds f1 . x = f2 . x

proof

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

end;

hence f1 = f2 ; :: thesis: verum