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: ( 0 .--> a = {} & {} = <*> A ) by FINSEQ_2:58;
A2: 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 A3: |.(n .--> a).| . a = n ; :: thesis: S₁[n + 1]
thus |.((n + 1) .--> a).| . a = |.((n .--> a) ^ <*a*>).| . a by FINSEQ_2:60
.= (|.(n .--> a).| [*] (chi a)) . a by Th40
.= n + ((chi a) . a) by A3, Th30
.= n + 1 by Th32 ; :: thesis: verum

end;

(A --> 0) . a = 0 by FUNCOP_1:7;
then A4: S₁[ 0 ] by A1, Th38;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A4, A2);
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 ;
A6: 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 A7: |.(n .--> a).| . b = 0 ; :: thesis: S₂[n + 1]
thus |.((n + 1) .--> a).| . b = |.((n .--> a) ^ <*a*>).| . b by FINSEQ_2:60
.= (|.(n .--> a).| [*] (chi a)) . b by Th40
.= 0 + ((chi a) . b) by A7, Th30
.= 0 by A5, Th32 ; :: thesis: verum

end;

(A --> 0) . b = 0 by FUNCOP_1:7;
then A8: S₂[ 0 ] by A1, Th38;
for n being Element of NAT holds S₂[n] from NAT_1:sch 1(A8, A6);
hence |.(n .--> a).| . b = 0 ; :: thesis: verum