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 S1[ Nat] means |.((In (\$1,NAT)) .--> a).| . a = \$1;
A1: ( 0 .--> a = {} & {} = <*> A ) by FINSEQ_2:58;
A2: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A3: |.((In (n,NAT)) .--> a).| . a = n ; :: thesis: S1[n + 1]
thus |.((In ((n + 1),NAT)) .--> a).| . a = |.(((In (n,NAT)) .--> a) ^ <*a*>).| . a by FINSEQ_2:60
.= (|.((In (n,NAT)) .--> a).| [*] (chi a)) . a by Th39
.= n + ((chi a) . a) by
.= n + 1 by Th31 ; :: thesis: verum
end;
(A --> 0) . a = 0 ;
then A4: S1[ 0 ] by ;
for n being Nat holds S1[n] from NAT_1:sch 2(A4, A2);
then |.((In (n,NAT)) .--> a).| . a = n ;
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 S2[ Nat] means |.((In (\$1,NAT)) .--> a).| . b = 0 ;
A6: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume A7: |.((In (n,NAT)) .--> a).| . b = 0 ; :: thesis: S2[n + 1]
thus |.((In ((n + 1),NAT)) .--> a).| . b = |.(((In (n,NAT)) .--> a) ^ <*a*>).| . b by FINSEQ_2:60
.= (|.((In (n,NAT)) .--> a).| [*] (chi a)) . b by Th39
.= 0 + ((chi a) . b) by
.= 0 by ; :: thesis: verum
end;
(A --> 0) . b = 0 ;
then A8: S2[ 0 ] by ;
for n being Nat holds S2[n] from NAT_1:sch 2(A8, A6);
then S2[n] ;
hence
|.(n .--> a).| . b = 0 ; :: thesis: verum