let f, g be Function; :: thesis: ( dom f = NAT & f . 0 = {{}} & ( for n being Nat ex Q being FinSequence-membered set st
( Q = f . n & f . (n + 1) = Q ^ P ) ) & dom g = NAT & g . 0 = {{}} & ( for n being Nat ex Q being FinSequence-membered set st
( Q = g . n & g . (n + 1) = Q ^ P ) ) implies f = g )
assume that
A1: dom f = NAT and
A2: f . 0 = {{}} and
A3: for n being Nat ex Q being FinSequence-membered set st
( Q = f . n & f . (n + 1) = Q ^ P ) and
A4: dom g = NAT and
A5: g . 0 = {{}} and
A6: for n being Nat ex Q being FinSequence-membered set st
( Q = g . n & g . (n + 1) = Q ^ P ) ; :: thesis: f = g
defpred S₁[ Nat] means f . $1 = g . $1;
A15: S₁[ 0 ] by A2, A5;
A16: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A17: S₁[n] ; :: thesis: S₁[n + 1]
consider Q being FinSequence-membered set such that
A18: ( Q = f . n & f . (n + 1) = Q ^ P ) by A3;
consider R being FinSequence-membered set such that
A19: ( R = g . n & g . (n + 1) = R ^ P ) by A6;
thus S₁[n + 1] by A17, A18, A19; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A15, A16);
then for a being object st a in dom f holds
f . a = g . a by A1;
hence f = g by A1, A4, FUNCT_1:2; :: thesis: verum