let X, Y be non empty set ; 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; 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; 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; 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; 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; ( 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))] ) ) ) )
; 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 S1[ Nat] means for x being Element of X st l . x <= $1 holds
f1 . x = f2 . x;
A2:
S1[ 0 ]
A3:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume B0:
S1[
k]
;
S1[k + 1]
let x be
Element of
X;
( l . x <= k + 1 implies f1 . x = f2 . x )
assume B1:
l . x <= k + 1
;
f1 . x = f2 . x
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
hence
f1 = f2
; verum