let n be Element of NAT ; :: thesis: for A being non empty set
for a being Element of A holds
( |.(n .--> a).| . a = n & ( for b being Element of A st b <> a holds
|.(n .--> a).| . b = 0 ) )
let A be non empty set ; :: thesis: for a being Element of A holds
( |.(n .--> a).| . a = n & ( for b being Element of A st b <> a holds
|.(n .--> a).| . b = 0 ) )
let a be Element of A; :: thesis: ( |.(n .--> a).| . a = n & ( for b being Element of A st b <> a holds
|.(n .--> a).| . b = 0 ) )
defpred S₁[ Element of NAT ] means |.($1 .--> a).| . a = $1;
A1: ( (A --> 0 ) . a = 0 & 0 .--> a = {} & {} = <*> A ) by FINSEQ_2:72, FUNCOP_1:13;
then A2: S₁[ 0 ] by Th38;
A3: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: |.(n .--> a).| . a = n ; :: thesis: S₁[n + 1]
thus |.((n + 1) .--> a).| . a = |.((n .--> a) ^ <*a*>).| . a by FINSEQ_2:74
.= (|.(n .--> a).| [*] (chi a)) . a by Th40
.= n + ((chi a) . a) by A4, Th30
.= n + 1 by Th32 ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A3);
hence |.(n .--> a).| . a = n ; :: thesis: for b being Element of A st b <> a holds
|.(n .--> a).| . b = 0
let b be Element of A; :: thesis: ( b <> a implies |.(n .--> a).| . b = 0 )
assume A5: b <> a ; :: thesis: |.(n .--> a).| . b = 0
defpred S₂[ Element of NAT ] means |.($1 .--> a).| . b = 0 ;
(A --> 0 ) . b = 0 by FUNCOP_1:13;
then A6: S₂[ 0 ] by A1, Th38;
A7: for n being Element of NAT st S₂[n] holds
S₂[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₂[n] implies S₂[n + 1] )
assume A8: |.(n .--> a).| . b = 0 ; :: thesis: S₂[n + 1]
thus |.((n + 1) .--> a).| . b = |.((n .--> a) ^ <*a*>).| . b by FINSEQ_2:74
.= (|.(n .--> a).| [*] (chi a)) . b by Th40
.= 0 + ((chi a) . b) by A8, Th30
.= 0 by A5, Th32 ; :: thesis: verum

end;

for n being Element of NAT holds S₂[n] from NAT_1:sch 1(A6, A7);
hence |.(n .--> a).| . b = 0 ; :: thesis: verum