let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being non empty AMI-Struct of IL,N
for A being set
for la being Object of S st ObjectKind la = A holds
for a being Element of A holds la .--> a is FinPartState of S
let N be with_non-empty_elements set ; :: thesis: for S being non empty AMI-Struct of IL,N
for A being set
for la being Object of S st ObjectKind la = A holds
for a being Element of A holds la .--> a is FinPartState of S
let S be non empty AMI-Struct of IL,N; :: thesis: for A being set
for la being Object of S st ObjectKind la = A holds
for a being Element of A holds la .--> a is FinPartState of S
let A be set ; :: thesis: for la being Object of S st ObjectKind la = A holds
for a being Element of A holds la .--> a is FinPartState of S
let la be Object of S; :: thesis: ( ObjectKind la = A implies for a being Element of A holds la .--> a is FinPartState of S )
assume A1: ObjectKind la = A ; :: thesis: for a being Element of A holds la .--> a is FinPartState of S
let a be Element of A; :: thesis: la .--> a is FinPartState of S
set p = la .--> a;
A2: dom (la .--> a) = {la} by FUNCOP_1:19;
A3: dom the Object-Kind of S = the carrier of S by FUNCT_2:def 1;

now

let x be set ; :: thesis: ( x in dom (la .--> a) implies (la .--> a) . x in the Object-Kind of S . x )
assume x in dom (la .--> a) ; :: thesis: (la .--> a) . x in the Object-Kind of S . x
then A4: x = la by A2, TARSKI:def 1;
then (la .--> a) . x = a by FUNCOP_1:87;
hence (la .--> a) . x in the Object-Kind of S . x by A1, A4; :: thesis: verum

end;

then reconsider p = la .--> a as Element of sproduct the Object-Kind of S by A2, A3, CARD_3:def 9;
p is FinPartState of S ;
hence la .--> a is FinPartState of S ; :: thesis: verum