let F1, F2 be Function of [: the carrier of H,( the carrier of H *):],( the carrier of H *); :: thesis: ( ( for x being Point of H
for e being FinSequence of H ex Fe being FinSequence of H st
( Fe = F1 . (x,e) & Fe = (x .|. e) (*) e ) ) & ( for x being Point of H
for e being FinSequence of H ex Fe being FinSequence of H st
( Fe = F2 . (x,e) & Fe = (x .|. e) (*) e ) ) implies F1 = F2 )
assume A1: for x being Point of H
for e being FinSequence of H ex Fe being FinSequence of H st
( Fe = F1 . (x,e) & Fe = (x .|. e) (*) e ) ; :: thesis: ( ex x being Point of H ex e being FinSequence of H st
for Fe being FinSequence of H holds
( not Fe = F2 . (x,e) or not Fe = (x .|. e) (*) e ) or F1 = F2 )
assume A2: for x being Point of H
for e being FinSequence of H ex Fe being FinSequence of H st
( Fe = F2 . (x,e) & Fe = (x .|. e) (*) e ) ; :: thesis: F1 = F2
set CH = the carrier of H;
for z, w being set st z in the carrier of H & w in the carrier of H * holds
F1 . (z,w) = F2 . (z,w)

proof

let z, w be set ; :: thesis: ( z in the carrier of H & w in the carrier of H * implies F1 . (z,w) = F2 . (z,w) )
assume A3: ( z in the carrier of H & w in the carrier of H * ) ; :: thesis: F1 . (z,w) = F2 . (z,w)
then reconsider x = z as Point of H ;
reconsider e = w as FinSequence of the carrier of H by A3, FINSEQ_1:def 11;
A4: ex Fe1 being FinSequence of H st
( Fe1 = F1 . (x,e) & Fe1 = (x .|. e) (*) e ) by A1;
ex Fe2 being FinSequence of H st
( Fe2 = F2 . (x,e) & Fe2 = (x .|. e) (*) e ) by A2;
hence F1 . (z,w) = F2 . (z,w) by A4; :: thesis: verum

end;

hence F1 = F2 ; :: thesis: verum