let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty COM-Struct of N
for A being set
for la being Object of S st the Object-Kind of S . la = A holds
for a being Element of A holds la .--> a is FinPartState of S
let S be non empty COM-Struct of N; :: thesis: for A being set
for la being Object of S st the Object-Kind of S . 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 the Object-Kind of S . la = A holds
for a being Element of A holds la .--> a is FinPartState of S
let la be Object of S; :: thesis: ( the Object-Kind of S . la = A implies for a being Element of A holds la .--> a is FinPartState of S )
assume A1: the Object-Kind of S . 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: 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;

reconsider p = la .--> a as PartState of S by A3, FUNCT_1:def 20;
p is PartState of S ;
hence la .--> a is FinPartState of S ; :: thesis: verum