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