let n be Nat; :: thesis: for a being set holds product (n |-> {a}) = {(n |-> a)}

let a be set ; :: thesis: product (n |-> {a}) = {(n |-> a)}

let a be set ; :: thesis: product (n |-> {a}) = {(n |-> a)}

now :: thesis: for i being object holds

( ( i in product (n |-> {a}) implies i = n |-> a ) & ( i = n |-> a implies i in product (n |-> {a}) ) )

hence
product (n |-> {a}) = {(n |-> a)}
by TARSKI:def 1; :: thesis: verum( ( i in product (n |-> {a}) implies i = n |-> a ) & ( i = n |-> a implies i in product (n |-> {a}) ) )

let i be object ; :: thesis: ( ( i in product (n |-> {a}) implies i = n |-> a ) & ( i = n |-> a implies i in product (n |-> {a}) ) )

then reconsider g = i as Function ;

.= dom (n |-> {a}) ;

hence i in product (n |-> {a}) by A7, CARD_3:9; :: thesis: verum

end;hereby :: thesis: ( i = n |-> a implies i in product (n |-> {a}) )

assume A6:
i = n |-> a
; :: thesis: i in product (n |-> {a})assume
i in product (n |-> {a})
; :: thesis: i = n |-> a

then consider g being Function such that

A1: i = g and

A2: dom g = dom (n |-> {a}) and

A3: for x being object st x in dom (n |-> {a}) holds

g . x in (n |-> {a}) . x by CARD_3:def 5;

A4: dom g = Seg n by A2;

end;then consider g being Function such that

A1: i = g and

A2: dom g = dom (n |-> {a}) and

A3: for x being object st x in dom (n |-> {a}) holds

g . x in (n |-> {a}) . x by CARD_3:def 5;

A4: dom g = Seg n by A2;

now :: thesis: for x being object st x in dom g holds

g . x = a

hence
i = n |-> a
by A1, A4, FUNCOP_1:11; :: thesis: verumg . x = a

let x be object ; :: thesis: ( x in dom g implies g . x = a )

assume A5: x in dom g ; :: thesis: g . x = a

then g . x in (n |-> {a}) . x by A2, A3;

then g . x in {a} by A4, A5, FUNCOP_1:7;

hence g . x = a by TARSKI:def 1; :: thesis: verum

end;assume A5: x in dom g ; :: thesis: g . x = a

then g . x in (n |-> {a}) . x by A2, A3;

then g . x in {a} by A4, A5, FUNCOP_1:7;

hence g . x = a by TARSKI:def 1; :: thesis: verum

then reconsider g = i as Function ;

A7: now :: thesis: for x being object st x in dom (n |-> {a}) holds

g . x in (n |-> {a}) . x

dom g =
Seg n
by A6
g . x in (n |-> {a}) . x

let x be object ; :: thesis: ( x in dom (n |-> {a}) implies g . x in (n |-> {a}) . x )

assume x in dom (n |-> {a}) ; :: thesis: g . x in (n |-> {a}) . x

then x in Seg n ;

then ( g . x = a & (n |-> {a}) . x = {a} ) by A6, FUNCOP_1:7;

hence g . x in (n |-> {a}) . x by TARSKI:def 1; :: thesis: verum

end;assume x in dom (n |-> {a}) ; :: thesis: g . x in (n |-> {a}) . x

then x in Seg n ;

then ( g . x = a & (n |-> {a}) . x = {a} ) by A6, FUNCOP_1:7;

hence g . x in (n |-> {a}) . x by TARSKI:def 1; :: thesis: verum

.= dom (n |-> {a}) ;

hence i in product (n |-> {a}) by A7, CARD_3:9; :: thesis: verum