let f be Function; :: thesis: for n being Element of NAT
for p1, p2 being Function of NAT ,(PFuncs ((dom f) \/ (rng f)),((dom f) \/ (rng f))) st p1 . 0 = id ((dom f) \/ (rng f)) & ( for k being Nat ex g being Function st
( g = p1 . k & p1 . (k + 1) = g * f ) ) & p2 . 0 = id ((dom f) \/ (rng f)) & ( for k being Nat ex g being Function st
( g = p2 . k & p2 . (k + 1) = g * f ) ) holds
p1 = p2
let n be Element of NAT ; :: thesis: for p1, p2 being Function of NAT ,(PFuncs ((dom f) \/ (rng f)),((dom f) \/ (rng f))) st p1 . 0 = id ((dom f) \/ (rng f)) & ( for k being Nat ex g being Function st
( g = p1 . k & p1 . (k + 1) = g * f ) ) & p2 . 0 = id ((dom f) \/ (rng f)) & ( for k being Nat ex g being Function st
( g = p2 . k & p2 . (k + 1) = g * f ) ) holds
p1 = p2
let p1, p2 be Function of NAT ,(PFuncs ((dom f) \/ (rng f)),((dom f) \/ (rng f))); :: thesis: ( p1 . 0 = id ((dom f) \/ (rng f)) & ( for k being Nat ex g being Function st
( g = p1 . k & p1 . (k + 1) = g * f ) ) & p2 . 0 = id ((dom f) \/ (rng f)) & ( for k being Nat ex g being Function st
( g = p2 . k & p2 . (k + 1) = g * f ) ) implies p1 = p2 )
assume that
A1: ( p1 . 0 = id ((dom f) \/ (rng f)) & ( for k being Nat ex g being Function st
( g = p1 . k & p1 . (k + 1) = g * f ) ) ) and
A2: ( p2 . 0 = id ((dom f) \/ (rng f)) & ( for k being Nat ex g being Function st
( g = p2 . k & p2 . (k + 1) = g * f ) ) ) ; :: thesis: p1 = p2
set FX = PFuncs ((dom f) \/ (rng f)),((dom f) \/ (rng f));
defpred S₁[ Nat, set , set ] means ex g being Function st
( g = $2 & $3 = g * f );
reconsider ID = id ((dom f) \/ (rng f)) as Element of PFuncs ((dom f) \/ (rng f)),((dom f) \/ (rng f)) by PARTFUN1:119;
A3: p1 . 0 = ID by A1;
B3: for k being Nat holds S₁[k,p1 . k,p1 . (k + 1)] by A1;
A4: p2 . 0 = ID by A2;
B4: for k being Nat holds S₁[k,p2 . k,p2 . (k + 1)] by A2;
A5: for k being Nat
for x, y1, y2 being Element of PFuncs ((dom f) \/ (rng f)),((dom f) \/ (rng f)) st S₁[k,x,y1] & S₁[k,x,y2] holds
y1 = y2 ;
p1 = p2 from NAT_1:sch 14(A3, B3, A4, B4, A5);
hence p1 = p2 ; :: thesis: verum