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)) and
A2: for k being Nat ex g being Function st
( g = p1 . k & p1 . (k + 1) = g * f ) and
A3: p2 . 0 = id ((dom f) \/ (rng f)) and
A4: for k being Nat ex g being Function st
( g = p2 . k & p2 . (k + 1) = g * f ) ; :: thesis: p1 = p2
defpred S₁[ Nat, set , set ] means ex g being Function st
( g = $2 & $3 = g * f );
A5: for k being Nat holds S₁[k,p1 . k,p1 . (k + 1)] by A2;
set FX = PFuncs ((dom f) \/ (rng f)),((dom f) \/ (rng f));
reconsider ID = id ((dom f) \/ (rng f)) as Element of PFuncs ((dom f) \/ (rng f)),((dom f) \/ (rng f)) by PARTFUN1:119;
A6: p2 . 0 = ID by A3;
A7: 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 ;
A8: for k being Nat holds S₁[k,p2 . k,p2 . (k + 1)] by A4;
A9: p1 . 0 = ID by A1;
p1 = p2 from NAT_1:sch 14(A9, A5, A6, A8, A7);
hence p1 = p2 ; :: thesis: verum