let f be Function; :: thesis: for n being Element of NAT
for p1, p2 being Function of NAT,(PFuncs ((field f),(field f))) st p1 . 0 = id (field f) & ( for k being Nat holds p1 . (k + 1) = (p1 . k) * f ) & p2 . 0 = id (field f) & ( for k being Nat holds p2 . (k + 1) = (p2 . k) * f ) holds
p1 = p2
let n be Element of NAT ; :: thesis: for p1, p2 being Function of NAT,(PFuncs ((field f),(field f))) st p1 . 0 = id (field f) & ( for k being Nat holds p1 . (k + 1) = (p1 . k) * f ) & p2 . 0 = id (field f) & ( for k being Nat holds p2 . (k + 1) = (p2 . k) * f ) holds
p1 = p2
let p1, p2 be Function of NAT,(PFuncs ((field f),(field f))); :: thesis: ( p1 . 0 = id (field f) & ( for k being Nat holds p1 . (k + 1) = (p1 . k) * f ) & p2 . 0 = id (field f) & ( for k being Nat holds p2 . (k + 1) = (p2 . k) * f ) implies p1 = p2 )
assume that
A1: p1 . 0 = id (field f) and
A2: for k being Nat holds p1 . (k + 1) = (p1 . k) * f and
A3: p2 . 0 = id (field f) and
A4: for k being Nat holds p2 . (k + 1) = (p2 . k) * f ; :: thesis: p1 = p2
defpred S₁[ Nat, Function, set ] means $3 = $2 * f;
A5: for k being Nat holds S₁[k,p1 . k,p1 . (k + 1)] by A2;
set FX = PFuncs ((field f),(field f));
reconsider ID = id (field f) as Element of PFuncs ((field f),(field f)) by PARTFUN1:119;
A6: p2 . 0 = ID by A3;
A7: for k being Nat
for x, y1, y2 being Element of PFuncs ((field f),(field 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